Informal definitions and lemmas

def Informal.isInformal : Lean.ConstantInfo → Bool

Is true if and only if a ConstantInfo corresponds to an InformalLemma or a InformalDefinition.

Equations

• Informal.isInformal (Lean.ConstantInfo.defnInfo c) = decide (c.type.isConstOf `InformalDefinition = true ∨ c.type.isConstOf `InformalLemma = true)
• Informal.isInformal x✝ = false

def Informal.isInformalLemma : Lean.ConstantInfo → Bool

Is true if and only if a ConstantInfo corresponds to an InformalLemma.

Equations

• Informal.isInformalLemma (Lean.ConstantInfo.defnInfo c) = c.type.isConstOf `InformalLemma
• Informal.isInformalLemma x✝ = false

def Informal.isInformalDef : Lean.ConstantInfo → Bool

Is true if and only if a ConstantInfo corresponds to an InformalDefinition.

Equations

• Informal.isInformalDef (Lean.ConstantInfo.defnInfo c) = c.type.isConstOf `InformalDefinition
• Informal.isInformalDef x✝ = false

unsafe def Informal.constantInfoToInformalLemma (c : Lean.ConstantInfo) : Lean.CoreM InformalLemma

Takes a ConstantInfo corresponding to a InformalLemma and returns the corresponding InformalLemma.

Equations

• One or more equations did not get rendered due to their size.
• Informal.constantInfoToInformalLemma (Lean.ConstantInfo.defnInfo c_1) = Lean.evalConstCheck InformalLemma `InformalLemma c_1.name

unsafe def Informal.constantInfoToInformalDefinition (c : Lean.ConstantInfo) : Lean.CoreM InformalDefinition

Takes a ConstantInfo corresponding to a InformalDefinition and returns the corresponding InformalDefinition.

Equations

• One or more equations did not get rendered due to their size.
• Informal.constantInfoToInformalDefinition (Lean.ConstantInfo.defnInfo c_1) = Lean.evalConstCheck InformalDefinition `InformalDefinition c_1.name

def PhysLean.noInformalLemmas : Lean.CoreM Nat

The number of informal lemmas in PhysLean.

Equations

• One or more equations did not get rendered due to their size.

def PhysLean.noInformalDefs : Lean.CoreM Nat

The number of informal definitions in PhysLean.

Equations

• One or more equations did not get rendered due to their size.