diff options
| author | Son Ho | 2023-07-04 18:09:36 +0200 |
|---|---|---|
| committer | Son Ho | 2023-07-04 18:09:36 +0200 |
| commit | b643bd00747e75d69b6066c55a1798b61277c4b6 (patch) | |
| tree | 84bbebe82964efc0d779ea782f3ae4b946ca3483 /tests/lean/Constants.lean | |
| parent | 74b3ce71b0e3794853aa1413afaaaa05c8cc5a84 (diff) | |
Regenerate the Lean test files
Diffstat (limited to '')
| -rw-r--r-- | tests/lean/Constants.lean | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/tests/lean/Constants.lean b/tests/lean/Constants.lean index cd2f88f5..9f6a47de 100644 --- a/tests/lean/Constants.lean +++ b/tests/lean/Constants.lean @@ -3,6 +3,8 @@ import Base open Primitives +namespace Constants + /- [constants::X0] -/ def x0_body : Result U32 := Result.ret (U32.ofInt 0 (by intlit)) def x0_c : U32 := eval_global x0_body (by simp) @@ -130,3 +132,4 @@ def s4_body : Result (pair_t U32 U32) := mk_pair1_fwd (U32.ofInt 7 (by intlit)) (U32.ofInt 8 (by intlit)) def s4_c : pair_t U32 U32 := eval_global s4_body (by simp) +end Constants |