summaryrefslogtreecommitdiff
path: root/tests/lean/Paper.lean
diff options
context:
space:
mode:
Diffstat (limited to 'tests/lean/Paper.lean')
-rw-r--r--tests/lean/Paper.lean5
1 files changed, 2 insertions, 3 deletions
diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean
index edcb5c1b..c34941ef 100644
--- a/tests/lean/Paper.lean
+++ b/tests/lean/Paper.lean
@@ -2,8 +2,7 @@
-- [paper]
import Base
open Primitives
-
-namespace Paper
+namespace paper
/- [paper::ref_incr] -/
def ref_incr_fwd_back (x : I32) : Result I32 :=
@@ -125,4 +124,4 @@ def call_choose_fwd (p : (U32 × U32)) : Result U32 :=
let (px0, _) ← choose_back U32 true px py pz0
Result.ret px0
-end Paper
+end paper