clean up ML module

lecopivo · Dec 4, 2023 · f4195e2 · f4195e2
1 parent 09f2449
commit f4195e2
Show file tree

Hide file tree

Showing 4 changed files with 195 additions and 356 deletions.
diff --git a/SciLean/Data/ArrayType/Notation.lean b/SciLean/Data/ArrayType/Notation.lean
@@ -65,12 +65,12 @@ abbrev introElemNotation {Cont Idx Elem} [ArrayType Cont Idx Elem] [ArrayTypeNot
   := introElem (Cont := arrayTypeCont Idx Elem) f
 
 open Lean.TSyntax.Compat in
-macro "⊞ " xs:Lean.explicitBinders " => " b:term:51 : term => Lean.expandExplicitBinders ``introElemNotation xs b
+macro "⊞ " x:term " => " b:term:51 : term => `(introElem fun $x => $b)
 
 @[app_unexpander introElemNotation] 
 def unexpandIntroElemNotation : Lean.PrettyPrinter.Unexpander
-  | `($(_) fun $x:ident => $b) => 
-    `(⊞ $x:ident => $b)
+  | `($(_) fun $x:term => $b) => 
+    `(⊞ $x:term => $b)
   | _  => throw ()