Documentation

Lean.Meta.Injective

def Lean.Meta.elimOptParam (type : Lean.Expr) :

Lean.CoreM Lean.Expr

Equations

Lean.Meta.elimOptParam type = Lean.Core.transform type (fun e => if Lean.Expr.isAppOfArity e `optParam 2 = true then pure (Lean.TransformStep.visit (Lean.Expr.getArg! e 0 (Lean.Expr.getAppNumArgs e))) else pure (Lean.TransformStep.visit e)) fun e => pure (Lean.TransformStep.done e)

def Lean.Meta.mkInjectiveTheoremNameFor (ctorName : Lean.Name) :

Equations

Lean.Meta.mkInjectiveTheoremNameFor ctorName = ctorName ++ `inj

def Lean.Meta.mkInjectiveEqTheoremNameFor (ctorName : Lean.Name) :

Equations

Lean.Meta.mkInjectiveEqTheoremNameFor ctorName = ctorName ++ `injEq

constant Lean.Meta.genInjectivity :

Lean.Option Bool

def Lean.Meta.mkInjectiveTheorems (declName : Lean.Name) :

Lean.MetaM Unit

Equations

Lean.Meta.mkInjectiveTheorems declName = do let a ← Lean.getEnv let a_1 ← Lean.getOptions let a_2 ← Lean.Meta.isInductivePredicate declName if (Lean.Environment.contains a `Eq.propIntro && Lean.Option.get a_1 Lean.Meta.genInjectivity && !a_2) = true then do let info ← Lean.getConstInfoInduct declName if info.isUnsafe = true then pure PUnit.unit else do let r ← let col := info.ctors; forIn col PUnit.unit fun ctor r => do let ctorVal ← Lean.getConstInfoCtor ctor if ctorVal.numFields > 0 then do Lean.Meta.mkInjectiveTheorem ctorVal Lean.Meta.mkInjectiveEqTheorem ctorVal pure (ForInStep.yield PUnit.unit) else do pure PUnit.unit pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure PUnit.unit else pure PUnit.unit