diff options
| -rw-r--r-- | compiler/Extract.ml | 7 | ||||
| -rw-r--r-- | tests/lean/Traits/Types.lean | 20 |
2 files changed, 16 insertions, 11 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 19c3803b..ce423acf 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -4272,6 +4272,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter) let item_name = ctx_get_trait_const decl.def_id name ctx in let ty () = let inside = false in + F.pp_print_space fmt (); extract_ty ctx fmt TypeDeclId.Set.empty inside ty in extract_trait_decl_item ctx fmt item_name ty) @@ -4282,7 +4283,10 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter) (fun (name, (clauses, _)) -> (* Extract the type *) let item_name = ctx_get_trait_type decl.def_id name ctx in - let ty () = F.pp_print_string fmt (type_keyword ()) in + let ty () = + F.pp_print_space fmt (); + F.pp_print_string fmt (type_keyword ()) + in extract_trait_decl_item ctx fmt item_name ty; (* Extract the clauses *) List.iter @@ -4291,6 +4295,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter) ctx_get_trait_item_clause decl.def_id name clause.clause_id ctx in let ty () = + F.pp_print_space fmt (); extract_trait_clause_type ctx fmt TypeDeclId.Set.empty clause in extract_trait_decl_item ctx fmt item_name ty) 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 |