Merge branch 'main' into us/calldecl-support

reilabs · Dec 27, 2024 · 6ea9c68 · 6ea9c68
2 parents e977b28 + 0b7d5f3
commit 6ea9c68
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/Lampe/Lampe/Syntax.lean b/Lampe/Lampe/Syntax.lean
@@ -93,6 +93,7 @@ syntax "*(" nr_expr ")" : nr_expr
 syntax "|" nr_param_decl,* "|" "->" nr_type nr_expr : nr_expr
 
 syntax nr_typed_expr := nr_expr ":" nr_type
+
 syntax "(" ident "as" nr_ident "<" nr_type,* ">" ")" "." ident : nr_expr -- Struct access
 syntax nr_ident "<" nr_type,* ">" "{" nr_expr,* "}" : nr_expr -- Struct constructor
 
@@ -101,6 +102,7 @@ syntax "(" nr_type "as" nr_ident "<" nr_type,* ">" ")" "::" nr_ident "<" nr_type
 syntax "^" nr_ident "(" nr_expr,* ")" ":" nr_type : nr_expr -- Lambda call
 syntax "@" nr_ident "<" nr_type,* ">" "(" nr_expr,* ")" ":" nr_type : nr_expr -- Decl call
 
+
 syntax nr_fn_decl := nr_ident "<" ident,* ">" "(" nr_param_decl,* ")" "->" nr_type "{" sepBy(nr_expr, ";", ";", allowTrailingSep) "}"
 syntax nr_trait_constraint := nr_type ":" nr_ident "<" nr_type,* ">"
 syntax nr_trait_fn_def := "fn" nr_fn_decl