Constructing inclusions

This file defines the main drivers of the inclusion tactic.

Given an expression e, mkExprInclusionBody recursively applies InclusionExts to construct an ExprInclusionBody for e. Then toExprInclusion applies HypothesisExts to the local context to construct inclusion hypotheses for the body's inclusion variables and closes the body into an ExprInclusion.

def Inclusion.mkExprInclusionBody (e : Lean.Expr) : InclusionM ExprInclusionBody

Construct an ExprInclusionBody for e.

Equations

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

def Inclusion.ExprInclusionBody.inferIType (body : ExprInclusionBody) (e : Lean.Expr) : Lean.MetaM IType

Check that body.proofBody is a proof of e ∈ body.inclusionBody and infer its IType.

Equations

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

def Inclusion.runHypothesisExts (h : Lean.Expr) : HypothesisM Unit

Run hypothesis extensions on hypothesis h.

Equations

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

def Inclusion.collectHyps : HypothesisM Unit

Run hypothesis extensions on all declarations in the local context.

Equations

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

def Inclusion.mkUniversalHypBody (iExpr : IExpr) : Lean.MetaM ExprInclusionBody

Construct the universal inclusion body for iExpr.

Equations

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

def Inclusion.combineHypBodies (iExpr : IExpr) (bodies : Array ExprInclusionBody) : Lean.MetaM ExprInclusionBody

Combine the candidate hypothesis bodies for iExpr using Refine, or use its Univ instance when there are no candidates.

Equations

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

def Inclusion.mkExprInclusion (output : IExpr) (body : ExprInclusionBody) : HypothesisM ExprInclusion

Given an output : IExpr and a body : ExprInclusionBody, construct an ExprInclusion for output.expr by collecting inclusion hypotheses from the local context and closing the body.

Equations

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

def Inclusion.toExprInclusion (e : Lean.Expr) : InclusionM ExprInclusion

Construct an ExprInclusion for e.

Equations

• Inclusion.toExprInclusion e = do let body ← Inclusion.mkExprInclusionBody e let iType ← liftM (body.inferIType e) (Inclusion.mkExprInclusion { iType := iType, expr := e } body).run