fix: f a <| do b => f a do b, not (f a) do b

leanprover-community · Jan 14, 2023 · 2bfc0cb · 2bfc0cb
1 parent 839a365
commit 2bfc0cb
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/Mathport/Syntax/Transform/Expr.lean b/Mathport/Syntax/Transform/Expr.lean
@@ -6,6 +6,9 @@ Authors: Gabriel Ebner
 import Mathport.Syntax.Transform.Basic
 
 mathport_rules
+  | `($x:term $args* <| fun $y:basicFun) => `($x:term $args* fun $y:basicFun)
+  | `($x:term $args* <| fun $y:matchAlts) => `($x:term $args* fun $y:matchAlts)
+  | `($x:term $args* <| do $s:doSeq) => `($x:term $args* do $s:doSeq)
   | `($x:term <| fun $y:basicFun) => `($x:term fun $y:basicFun)
   | `($x:term <| fun $y:matchAlts) => `($x:term fun $y:matchAlts)
   | `($x:term <| do $s:doSeq) => `($x:term do $s:doSeq)