diff options
author | Son Ho | 2023-10-06 12:23:26 +0200 |
---|---|---|
committer | Son Ho | 2023-10-06 12:23:26 +0200 |
commit | af78286d801b26bf7a70b8815619591d48245cb8 (patch) | |
tree | 73ba66fe81fa45b4421922abc8e2e19667e98153 /tests | |
parent | e684179ff9c582495b720c3b1310e0648ca24a58 (diff) |
Slightly improve formatting of the generated code
Diffstat (limited to '')
-rw-r--r-- | tests/lean/Traits/Types.lean | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/tests/lean/Traits/Types.lean b/tests/lean/Traits/Types.lean index b3a52346..a8c12fe5 100644 --- a/tests/lean/Traits/Types.lean +++ b/tests/lean/Traits/Types.lean @@ -48,11 +48,11 @@ structure BoolWrapper where /- Trait declaration: [traits::WithConstTy] -/ structure WithConstTy (Self : Type) (LEN : Usize) where - LEN1 :Usize - LEN2 :Usize - V :Type - W :Type - W_clause_0 :ToU64 W + LEN1 : Usize + LEN2 : Usize + V : Type + W : Type + W_clause_0 : ToU64 W f : W → Array U8 LEN → Result W /- [alloc::string::String] -/ @@ -60,7 +60,7 @@ axiom alloc.string.String : Type /- Trait declaration: [traits::ParentTrait0] -/ structure ParentTrait0 (Self : Type) where - W :Type + W : Type get_name : Self → Result alloc.string.String get_w : Self → Result W @@ -74,13 +74,13 @@ structure ChildTrait (Self : Type) where /- Trait declaration: [traits::Iterator] -/ structure Iterator (Self : Type) where - Item :Type + Item : Type /- Trait declaration: [traits::IntoIterator] -/ structure IntoIterator (Self : Type) where - Item :Type - IntoIter :Type - IntoIter_clause_0 :Iterator IntoIter + Item : Type + IntoIter : Type + IntoIter_clause_0 : Iterator IntoIter into_iter : Self → Result IntoIter end traits |