diff options
author | Son Ho | 2023-11-09 11:22:39 +0100 |
---|---|---|
committer | Son Ho | 2023-11-09 11:22:39 +0100 |
commit | eb9ff46c69b9a95c453d64eee059916130d59846 (patch) | |
tree | d66fdbdf8727731459498d3e05f155ce6c971354 /tests/lean/Traits/Funs.lean | |
parent | 9df1d191cfaf929b755e9d26d55811531acd939d (diff) |
Regenerate some Lean tests
Diffstat (limited to '')
-rw-r--r-- | tests/lean/Traits/Funs.lean | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/tests/lean/Traits/Funs.lean b/tests/lean/Traits/Funs.lean index 6a2834ff..8d423280 100644 --- a/tests/lean/Traits/Funs.lean +++ b/tests/lean/Traits/Funs.lean @@ -247,4 +247,29 @@ def map_option let t ← inst.call f0 x0 Result.ret (some t) +/- Trait implementation: [traits::u32::{11}] -/ +def u32.WithTargetInst : WithTarget U32 := { + Target := U32 +} + +/- Trait implementation: [traits::u32::{12}] -/ +def u32.ParentTrait2Inst : ParentTrait2 U32 := { + U := U32 + U_clause_0 := u32.WithTargetInst +} + +/- [traits::u32::{13}::convert]: forward function -/ +def u32.convert (x : U32) : Result U32 := + Result.ret x + +/- Trait implementation: [traits::u32::{13}] -/ +def u32.ChildTrait2Inst : ChildTrait2 U32 := { + parent_clause_0 := u32.ParentTrait2Inst + convert := u32.convert +} + +/- [traits::incr_u32]: forward function -/ +def incr_u32 (x : U32) : Result U32 := + x + 1#u32 + end traits |