From b643bd00747e75d69b6066c55a1798b61277c4b6 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 4 Jul 2023 18:09:36 +0200 Subject: Regenerate the Lean test files --- tests/lean/Constants.lean | 3 +++ 1 file changed, 3 insertions(+) (limited to 'tests/lean/Constants.lean') 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 -- cgit v1.2.3