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

fix: do not generate injectivity theorems for unsafe inductive datatypes

Browse source
This commit is contained in:
Leonardo de Moura 2021-05-14 17:37:41 -07:00
parent 175311b2f0
commit 05147fd352
1 changed files with 6 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -140,10 +140,11 @@ register_builtin_option genInjective : Bool := {
def mkInjectiveTheorems (declName : Name) : MetaM Unit := do
if (← getEnv).contains ``Eq.propIntro && genInjective.get (← getOptions) && !(← isInductivePredicate declName) then
let info ← getConstInfoInduct declName
for ctor in info.ctors do
let ctorVal ← getConstInfoCtor ctor
if ctorVal.numFields > 0 then
mkInjectiveTheorem ctorVal
mkInjectiveEqTheorem ctorVal
unless info.isUnsafe do
for ctor in info.ctors do
let ctorVal ← getConstInfoCtor ctor
if ctorVal.numFields > 0 then
mkInjectiveTheorem ctorVal
mkInjectiveEqTheorem ctorVal
end Lean.Meta