Merge remote-tracking branch 'origin/master' into refactor-macro-comp-2

alexkeizer · Jun 26, 2024 · dd04580 · dd04580
2 parents 6d15f94 + c62f9cc
commit dd04580
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/Qpf/Macro/Comp.lean b/Qpf/Macro/Comp.lean
@@ -249,7 +249,6 @@ partial def handleApp (vars : Vector FVarId arity) (target : Q(Type u))  : TermE
 partial def handleArrow (binderType body : Expr) (vars : Vector FVarId arity) (targetStx : Option Term := none) (normalized := false): TermElabM (ElabQpfResult u arity) := do
   let newTarget ← mkAppM ``MvQPF.Arrow.Arrow #[binderType, body]
   elabQpf vars newTarget targetStx normalized
-
 /--
   Elaborate the body of a qpf
 -/