small fixes

reilabs · Dec 27, 2024 · c65feaa · c65feaa
1 parent d1a1d1f
commit c65feaa
Showing 1 changed file with 0 additions and 6 deletions.
diff --git a/Lampe/Lampe/Syntax.lean b/Lampe/Lampe/Syntax.lean
@@ -39,12 +39,6 @@ syntax "[" nr_type "]" : nr_type -- Slice
 syntax "[" nr_type ";" num "]" : nr_type -- Array
 syntax "`(" nr_type,* ")" : nr_type -- Tuple
 
-def mkFieldName (structName : String) (fieldName : String) : Lean.Ident :=
-  mkIdent $ Name.mkSimple $ "field" ++ "#" ++ structName ++ "#" ++ fieldName
-
-def mkStructDefIdent (structName : String) : Lean.Ident :=
-   mkIdent $ Name.mkSimple $ "struct" ++ "#" ++ structName
-
 def mkFieldName (structName : String) (fieldName : String) : Lean.Ident :=
   mkIdent $ Name.mkSimple $ "field" ++ "#" ++ structName ++ "#" ++ fieldName