fix array lambda notation

lecopivo · Dec 5, 2023 · 384ddc4 · 384ddc4
1 parent 4063def
commit 384ddc4
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/SciLean/Data/ArrayType/Notation.lean b/SciLean/Data/ArrayType/Notation.lean
@@ -66,6 +66,7 @@ abbrev introElemNotation {Cont Idx Elem} [ArrayType Cont Idx Elem] [ArrayTypeNot
 
 open Lean.TSyntax.Compat in
 macro "⊞ " x:term " => " b:term:51 : term => `(introElemNotation fun $x => $b)
+macro "⊞ " x:term " : " X:term " => " b:term:51 : term => `(introElemNotation fun ($x : $X) => $b)
 
 @[app_unexpander introElemNotation] 
 def unexpandIntroElemNotation : Lean.PrettyPrinter.Unexpander