Lean.Meta.Constructions

def Lean.mkRecOn {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] [inst : Lean.MonadOptions m] (declName : Lean.Name) :

m Unit

Equations

Lean.mkRecOn declName = Lean.adaptFn Lean.mkRecOnImp declName

source

def Lean.mkNoConfusionCore {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] [inst : Lean.MonadOptions m] (declName : Lean.Name) :

m Unit

Equations

Lean.mkNoConfusionCore declName = Lean.adaptFn Lean.mkNoConfusionCoreImp declName

source

def Lean.mkBelow {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] [inst : Lean.MonadOptions m] (declName : Lean.Name) :

m Unit

Equations

Lean.mkBelow declName = Lean.adaptFn Lean.mkBelowImp declName

source

def Lean.mkIBelow {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] [inst : Lean.MonadOptions m] (declName : Lean.Name) :

m Unit

Equations

Lean.mkIBelow declName = Lean.adaptFn Lean.mkIBelowImp declName

source

def Lean.mkBRecOn {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] [inst : Lean.MonadOptions m] (declName : Lean.Name) :

m Unit

Equations

Lean.mkBRecOn declName = Lean.adaptFn Lean.mkBRecOnImp declName

source

def Lean.mkBInductionOn {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] [inst : Lean.MonadOptions m] (declName : Lean.Name) :

m Unit

Equations

Lean.mkBInductionOn declName = Lean.adaptFn Lean.mkBInductionOnImp declName

source

def Lean.mkNoConfusionEnum (enumName : Lean.Name) :

Lean.MetaM Unit

Equations

Lean.mkNoConfusionEnum enumName = (fun mkNoConfusion => do let a ← Lean.getEnv if Lean.Environment.contains a `noConfusionEnum = true then do mkToCtorIdx mkNoConfusionType mkNoConfusion else Lean.mkNoConfusionCore enumName) (Lean.mkNoConfusionEnum.mkToCtorIdx enumName) (Lean.mkNoConfusionEnum.mkNoConfusionType enumName) (Lean.mkNoConfusionEnum.mkNoConfusion enumName)

source

def Lean.mkNoConfusionEnum.mkToCtorIdx (enumName : Lean.Name) :

Lean.MetaM Unit

Equations

Lean.mkNoConfusionEnum.mkToCtorIdx enumName = do let discr ← Lean.getConstInfo enumName match discr with | Lean.ConstantInfo.inductInfo info => let numCtors := List.length info.ctors; let declName := Lean.Name.mkStr enumName "toCtorIdx"; let enumType := Lean.mkConst enumName; let natType := Lean.mkConst `Nat; do let declType ← Lean.Meta.mkArrow enumType natType let minors : Array Lean.Expr := #[] let r ← let col := { start := 0, stop := numCtors, step := 1 }; forIn col minors fun i r => let minors := r; let minors := Array.push minors (Lean.mkNatLit i); do pure PUnit.unit pure (ForInStep.yield minors) let x : Array Lean.Expr := r let minors : Array Lean.Expr := x Lean.Meta.withLocalDeclD `x enumType fun x => do let motive ← Lean.Meta.mkLambdaFVars #[x] natType false true let declValue ← Lean.Meta.mkLambdaFVars #[x] (Lean.mkAppN (Lean.mkApp2 (Lean.mkConst (Lean.mkCasesOnName enumName) [Lean.levelOne]) motive x) minors) false true Lean.addAndCompile (Lean.Declaration.defnDecl { toConstantVal := { name := declName, levelParams := [], type := declType }, value := declValue, hints := Lean.ReducibilityHints.abbrev, safety := Lean.DefinitionSafety.safe }) | x => panicWithPosWithDecl "Lean.Meta.Constructions" "Lean.mkNoConfusionEnum.mkToCtorIdx" 47 63 "unreachable code has been reached"

source

def Lean.mkNoConfusionEnum.mkNoConfusionType (enumName : Lean.Name) :

Lean.MetaM Unit

Equations

Lean.mkNoConfusionEnum.mkNoConfusionType enumName = let enumType := Lean.mkConst enumName; let sortU := Lean.mkSort (Lean.mkLevelParam `u); let toCtorIdx := Lean.mkConst (Lean.Name.mkStr enumName "toCtorIdx"); Lean.Meta.withLocalDeclD `P sortU fun P => Lean.Meta.withLocalDeclD `x enumType fun x => Lean.Meta.withLocalDeclD `y enumType fun y => do let declType ← Lean.Meta.mkForallFVars #[P, x, y] sortU false true let a ← Lean.Meta.mkAppM `noConfusionTypeEnum #[toCtorIdx, P, x, y] let declValue ← Lean.Meta.mkLambdaFVars #[P, x, y] a false true let declName : Lean.Name := Lean.Name.mkStr enumName "noConfusionType" Lean.addAndCompile (Lean.Declaration.defnDecl { toConstantVal := { name := declName, levelParams := [`u], type := declType }, value := declValue, hints := Lean.ReducibilityHints.abbrev, safety := Lean.DefinitionSafety.safe })

source

def Lean.mkNoConfusionEnum.mkNoConfusion (enumName : Lean.Name) :

Lean.MetaM Unit

Equations

Lean.mkNoConfusionEnum.mkNoConfusion enumName = let enumType := Lean.mkConst enumName; let u := Lean.mkLevelParam `u; let sortU := Lean.mkSort u; let toCtorIdx := Lean.mkConst (Lean.Name.mkStr enumName "toCtorIdx"); let noConfusionType := Lean.mkConst (Lean.Name.mkStr enumName "noConfusionType") [u]; Lean.Meta.withLocalDecl `P Lean.BinderInfo.implicit sortU fun P => Lean.Meta.withLocalDecl `x Lean.BinderInfo.implicit enumType fun x => Lean.Meta.withLocalDecl `y Lean.BinderInfo.implicit enumType fun y => do let a ← Lean.Meta.mkEq x y Lean.Meta.withLocalDeclD `h a fun h => do let declType ← Lean.Meta.mkForallFVars #[P, x, y, h] (Lean.mkApp3 noConfusionType P x y) false true let a ← Lean.Meta.mkAppOptM `noConfusionEnum #[none, none, none, some toCtorIdx, some P, some x, some y, some h] let declValue ← Lean.Meta.mkLambdaFVars #[P, x, y, h] a false true let declName : Lean.Name := Lean.Name.mkStr enumName "noConfusion" Lean.addAndCompile (Lean.Declaration.defnDecl { toConstantVal := { name := declName, levelParams := [`u], type := declType }, value := declValue, hints := Lean.ReducibilityHints.abbrev, safety := Lean.DefinitionSafety.safe })

source

def Lean.mkNoConfusion (declName : Lean.Name) :

Lean.MetaM Unit

Equations

Lean.mkNoConfusion declName = do let a ← Lean.isEnumType declName if a = true then Lean.mkNoConfusionEnum declName else Lean.mkNoConfusionCore declName