From 384ddc419864fa21e1ebde364c0ea4b85843fff9 Mon Sep 17 00:00:00 2001 From: lecopivo Date: Tue, 5 Dec 2023 11:55:19 -0500 Subject: [PATCH] fix array lambda notation --- SciLean/Data/ArrayType/Notation.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/SciLean/Data/ArrayType/Notation.lean b/SciLean/Data/ArrayType/Notation.lean index 0043c474..708c73b8 100644 --- 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