diff options
| author | Son Ho | 2023-10-27 12:12:18 +0200 |
|---|---|---|
| committer | Son Ho | 2023-10-27 12:12:18 +0200 |
| commit | 4f824528f5e0c0f898b20917c6c06821efb934da (patch) | |
| tree | 0989906573fc3f0da6786974b36e81defe1fd9b5 /tests/lean/Constants.lean | |
| parent | 1110b3da85e93ba0755a665edd5b8c986c54cef0 (diff) | |
Regenerate some of the F* test files
Diffstat (limited to '')
| -rw-r--r-- | tests/lean/Constants.lean | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tests/lean/Constants.lean b/tests/lean/Constants.lean index 2603cbbf..bd3a07b7 100644 --- a/tests/lean/Constants.lean +++ b/tests/lean/Constants.lean @@ -56,11 +56,11 @@ def p3_c : Pair U32 U32 := eval_global p3_body (by simp) /- [constants::Wrap] -/ structure Wrap (T : Type) where - val : T + value : T /- [constants::Wrap::{0}::new]: forward function -/ -def Wrap.new (T : Type) (val : T) : Result (Wrap T) := - Result.ret { val := val } +def Wrap.new (T : Type) (value : T) : Result (Wrap T) := + Result.ret { value := value } /- [constants::Y] -/ def y_body : Result (Wrap I32) := Wrap.new I32 2#i32 @@ -68,7 +68,7 @@ def y_c : Wrap I32 := eval_global y_body (by simp) /- [constants::unwrap_y]: forward function -/ def unwrap_y : Result I32 := - Result.ret y_c.val + Result.ret y_c.value /- [constants::YVAL] -/ def yval_body : Result I32 := unwrap_y |