max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

hack: ignore maxCoeSize for monad coercions

Browse source
This commit is contained in:
Gabriel Ebner 2022-10-13 22:37:18 -07:00
parent 1c561c39a8
commit 045a71ab33
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Meta/Coe.lean
View file

@ -162,7 +162,7 @@ def coerceMonadLift? (e expectedType : Expr) : MetaM (Option Expr) := do
try
-- Construct lift from `m` to `n`
let monadLiftType ← mkAppM ``MonadLiftT #[m, n]
let .some monadLiftVal ← trySynthInstanceForCoe monadLiftType | return none
let .some monadLiftVal ← trySynthInstance monadLiftType | return none
let u_1 ← getDecLevel α
let u_2 ← getDecLevel eType
let u_3 ← getDecLevel expectedType
@ -175,7 +175,7 @@ def coerceMonadLift? (e expectedType : Expr) : MetaM (Option Expr) := do
let u ← getLevel α
let v ← getLevel β
let coeTInstType := Lean.mkForall `a BinderInfo.default α <| mkAppN (mkConst ``CoeT [u, v]) #[α, mkBVar 0, β]
let .some coeTInstVal ← trySynthInstanceForCoe coeTInstType | return none
let .some coeTInstVal ← trySynthInstance coeTInstType | return none
let eNew ← expandCoe (mkAppN (Lean.mkConst ``Lean.Internal.liftCoeM [u_1, u_2, u_3]) #[m, n, α, β, monadLiftVal, coeTInstVal, monadInst, e])
let eNewType ← inferType eNew
unless (← isDefEq expectedType eNewType) do return none