Skip to content

Commit

Permalink
Apply suggestions from code review
Browse files Browse the repository at this point in the history
Fix whitespace
  • Loading branch information
Equilibris authored Jun 28, 2024
1 parent 6e78b77 commit 76af185
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions Qpf/Macro/Comp.lean
Original file line number Diff line number Diff line change
Expand Up @@ -154,7 +154,7 @@ def DVec.toExpr {n : Nat} {αs : Q(Fin2 $n → Type u)} (xs : DVec (fun (i : Fin


structure ElabQpfResult (u : Level) (arity : Nat) where
F : Q(TypeFun.{u,u} $arity) := by exact q(by infer_instance)
F : Q(TypeFun.{u,u} $arity)
functor : Q(MvFunctor $F) := by exact q(by infer_instance)
qpf : Q(@MvQPF _ $F $functor) := by exact q(by infer_instance)
deriving Inhabited
Expand Down Expand Up @@ -183,7 +183,7 @@ partial def handleConst (target : Q(Type u)) : TermElabM (ElabQpfResult u arity
pure { F := const, functor := q(Const.MvFunctor), qpf := q(Const.mvqpf)}


partial def handleApp (vars : Vector FVarId arity) (target : Q(Type u)) : TermElabM (ElabQpfResult u arity) := do
partial def handleApp (vars : Vector FVarId arity) (target : Q(Type u)) : TermElabM (ElabQpfResult u arity) := do
let vars' := vars.toList

let ⟨numArgs, F, args⟩ ← (Comp.parseApp (isLiveVar vars) target)
Expand Down Expand Up @@ -236,7 +236,7 @@ partial def handleApp (vars : Vector FVarId arity) (target : Q(Type u)) : TermE
return { F := comp, functor, qpf }


partial def handleArrow (binderType body : Expr) (vars : Vector FVarId arity) (targetStx : Option Term := none) (normalized := false): TermElabM (ElabQpfResult u arity) := do
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
/--
Expand Down

0 comments on commit 76af185

Please sign in to comment.