From d9fd9bb1b3d9bfd5a08be2e79ef97bbd5c6deaab Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 5 Mar 2020 17:14:29 -0800 Subject: [PATCH] feat: add `mkEqOfHEq` --- src/Init/Lean/Meta/AppBuilder.lean | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/Init/Lean/Meta/AppBuilder.lean b/src/Init/Lean/Meta/AppBuilder.lean index 4c79ca4c06..0f5fb96d97 100644 --- a/src/Init/Lean/Meta/AppBuilder.lean +++ b/src/Init/Lean/Meta/AppBuilder.lean @@ -94,6 +94,16 @@ else do u ← getLevel α; pure $ mkApp8 (mkConst `HEq.trans [u]) α β γ a b c h₁ h₂ | _, _ => throwEx $ Exception.appBuilder `HEq.trans "heterogeneous equality proof expected" #[h₁, h₂] +def mkEqOfHEq (h : Expr) : MetaM Expr := do +hType ← infer h; +match hType.heq? with +| some (α, a, β, b) => do + unlessM (isDefEq α β) $ throwEx $ Exception.appBuilder `eqOfHEq "heterogeneous equality types are not definitionally equal" #[α, β]; + u ← getLevel α; + pure $ mkApp4 (mkConst `eqOfHEq [u]) α a b h +| _ => + throwEx $ Exception.appBuilder `HEq.trans "heterogeneous equality proof expected" #[h] + def mkCongrArg (f h : Expr) : MetaM Expr := do hType ← infer h; fType ← infer f;