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

feat: improve error message

Browse source
This commit is contained in:
Leonardo de Moura 2021-05-14 17:45:52 -07:00
parent 05147fd352
commit 0f43a338e6
2 changed files with 10 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/Lean/Meta/Injective.lean
View file

@ -69,8 +69,11 @@ private partial def mkInjectiveTheoremTypeCore? (ctorVal : ConstructorVal) (useE
private def mkInjectiveTheoremType? (ctorVal : ConstructorVal) : MetaM (Option Expr) :=
mkInjectiveTheoremTypeCore? ctorVal false
private def injTheoremFailureHeader (ctorName : Name) : MessageData :=
m!"failed to prove injectivity theorem for constructor '{ctorName}', use 'set_option genInjectivity false' to disable the generation"
private def throwInjectiveTheoremFailure {α} (ctorName : Name) (mvarId : MVarId) : MetaM α :=
throwError "failed to prove injective theorem for constructor '{ctorName}', use 'set_option genInjective false' to disable the generation{indentD <| MessageData.ofGoal mvarId}"
throwError "{injTheoremFailureHeader ctorName}{indentD <| MessageData.ofGoal mvarId}"
private def solveEqOfCtorEq (ctorName : Name) (mvarId : MVarId) (h : FVarId) : MetaM Unit := do
match (← injection mvarId h) with
@ -116,7 +119,7 @@ private def mkInjectiveEqTheoremValue (ctorName : Name) (targetType : Expr) : Me
solveEqOfCtorEq ctorName mvarId₁ h
let mvarId₂ ← casesAnd mvarId₂
let mvarId₂ ← substEqs mvarId₂
applyRefl mvarId₂
applyRefl mvarId₂ (injTheoremFailureHeader ctorName)
mkLambdaFVars xs mvar
private def mkInjectiveEqTheorem (ctorVal : ConstructorVal) : MetaM Unit := do
@ -132,13 +135,13 @@ private def mkInjectiveEqTheorem (ctorVal : ConstructorVal) : MetaM Unit := do
}
addSimpLemma name (post := true) AttributeKind.global (prio := eval_prio default)
register_builtin_option genInjective : Bool := {
register_builtin_option genInjectivity : Bool := {
defValue := true
descr := "generate injective theorems for inductive datatype constructors"
descr := "generate injectivity theorems for inductive datatype constructors"
}
def mkInjectiveTheorems (declName : Name) : MetaM Unit := do
if (← getEnv).contains ``Eq.propIntro && genInjective.get (← getOptions) && !(← isInductivePredicate declName) then
if (← getEnv).contains ``Eq.propIntro && genInjectivity.get (← getOptions) && !(← isInductivePredicate declName) then
let info ← getConstInfoInduct declName
unless info.isUnsafe do
for ctor in info.ctors do

4
src/Lean/Meta/Tactic/Apply.lean
View file

@ -101,9 +101,9 @@ def splitAnd (mvarId : MVarId) : MetaM (List MVarId) := do
saturate mvarId fun mvarId =>
observing? <| apply mvarId (mkConst ``And.intro)
def applyRefl (mvarId : MVarId) : MetaM Unit :=
def applyRefl (mvarId : MVarId) (msg : MessageData) : MetaM Unit :=
withMVarContext mvarId do
let some [] ← observing? do apply mvarId (mkConst ``Eq.refl [← mkFreshLevelMVar])
| throwTacticEx `refl mvarId ""
| throwTacticEx `refl mvarId msg
end Lean.Meta