Attributes for inclusion extensions

This file defines the attributes used to register inclusion and hypothesis extensions.

def Inclusion.inclusionParamAttr : Lean.ParserDescr

Syntax for registering an inclusion parameter using the inclusion_param attribute.

Equations

• Inclusion.inclusionParamAttr = Lean.ParserDescr.node `Inclusion.inclusionParamAttr 1024 (Lean.ParserDescr.nonReservedSymbol "inclusion_param" false)

def Inclusion.addInclusionParam (declName : Lean.Name) (kind : Lean.AttributeKind) : Lean.AttrM Unit

Add the inclusion parameter declared by declName.

Equations

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

def Inclusion.inclusionExtAttr : Lean.ParserDescr

Syntax for declaring an inclusion extension using the inclusion_ext attribute.

Equations

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

def Inclusion.addInclusionExt (declName : Lean.Name) (keys : Array (Array Lean.Meta.DiscrTree.Key)) (kind : Lean.AttributeKind) : Lean.AttrM Unit

Add the inclusion extension declName under keys.

Equations

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

def Inclusion.hypothesisExtAttr : Lean.ParserDescr

Syntax for declaring a hypothesis extension using the hypothesis_ext attribute.

Equations

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

def Inclusion.addHypothesisExt (declName : Lean.Name) (keys : Array (Array Lean.Meta.DiscrTree.Key)) (kind : Lean.AttributeKind) : Lean.AttrM Unit

Add the hypothesis extension declName under keys.

Equations

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

structure Inclusion.HypArg : Type

The argument indices of an element x, a set s, and an inclusion hypothesis x ∈ s in some theorem statement.

• elemIdx : ℕ

  The index of the element argument.

• setIdx : ℕ

  The index of the set argument.

• proofIdx : ℕ

  The index of the membership proof argument.

@[instance_reducible]

instance Inclusion.instInhabitedHypArg : Inhabited HypArg

Equations

• Inclusion.instInhabitedHypArg = { default := Inclusion.instInhabitedHypArg.default }

@[instance_reducible]

instance Inclusion.instToExprHypArg : Lean.ToExpr HypArg

Equations

• Inclusion.instToExprHypArg = { toExpr := Inclusion.instToExprHypArg.toExpr, toTypeExpr := Lean.Expr.const `Inclusion.HypArg [] }

def Inclusion.instToExprHypArg.toExpr : HypArg → Lean.Expr

Equations

• Inclusion.instToExprHypArg.toExpr { elemIdx := a, setIdx := a_1, proofIdx := a_2 } = (((Lean.Expr.const `Inclusion.HypArg.mk []).app (Lean.toExpr a)).app (Lean.toExpr a_1)).app (Lean.toExpr a_2)

structure Inclusion.ParamArg : Type

The name of an inclusion parameter and its index in some theorem statement.

• name : Lean.Name

  The name of the registered inclusion parameter.

• idx : ℕ

  The index of the corresponding theorem argument.

@[instance_reducible]

instance Inclusion.instInhabitedParamArg : Inhabited ParamArg

Equations

• Inclusion.instInhabitedParamArg = { default := Inclusion.instInhabitedParamArg.default }

def Inclusion.instToExprParamArg.toExpr : ParamArg → Lean.Expr

Equations

• Inclusion.instToExprParamArg.toExpr { name := a, idx := a_1 } = ((Lean.Expr.const `Inclusion.ParamArg.mk []).app (Lean.toExpr a)).app (Lean.toExpr a_1)

@[instance_reducible]

instance Inclusion.instToExprParamArg : Lean.ToExpr ParamArg

Equations

• Inclusion.instToExprParamArg = { toExpr := Inclusion.instToExprParamArg.toExpr, toTypeExpr := Lean.Expr.const `Inclusion.ParamArg [] }

def Inclusion.deriveInclusionOp (theoremName : Lean.Name) (hypArgs : Array HypArg) (paramArgs : Array ParamArg) (e : Lean.Expr) : InclusionM ExprInclusionBody

Apply the inclusion theorem theoremName to e, recursively constructing the inclusion bodies specified by hypArgs and filling the registered parameter arguments specified by paramArgs.

Equations

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

def Inclusion.deriveHypothesisOp (theoremName : Lean.Name) (sourceIdx : ℕ) (hypArgs : Array HypArg) (paramArgs : Array ParamArg) (h : Lean.Expr) : HypothesisM Unit

Apply the hypothesis theorem theoremName to h as its source hypothesis at sourceIdx, recursively constructing the closed inclusion bodies specified by hypArgs and filling the registered parameter arguments specified by paramArgs.

Equations

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

def Inclusion.inclusionOpAttr : Lean.ParserDescr

Syntax for registering an inclusion extension from a theorem using the inclusion_op attribute.

Equations

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

def Inclusion.hypothesisOpAttr : Lean.ParserDescr

Syntax for registering a hypothesis extension from a theorem using the hypothesis_op attribute.

Equations

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