def List.subsequences {α : Type u_1} (xs : List α) : List (List α)

Equations

• [].subsequences = [[]]
• (a :: as).subsequences = as.subsequences ++ List.map (List.cons a) as.subsequences

def Lean.getParamLevelName! : Level → Name

Equations

• One or more equations did not get rendered due to their size.
• Lean.getParamLevelName! (Lean.Level.param name) = name

def Lean.Expr.countLambdas : Expr → Nat

Equations

• (Lean.Expr.lam binderName binderType b binderInfo).countLambdas = b.countLambdas + 1
• x✝.countLambdas = 0

def Lean.Expr.countForalls : Expr → Nat

Equations

• (Lean.Expr.forallE binderName binderType b binderInfo).countForalls = b.countForalls + 1
• x✝.countForalls = 0

def Lean.Expr.instantiateForallNoReducing (e : Expr) (ps : Array Expr) : MetaM Expr

Given e of the form forall (a_1 : A_1) ... (a_n : A_n), B[a_1, ..., a_n] and p_1 : A_1, ... p_n : A_n, return B[p_1, ..., p_n].

Equations

• e.instantiateForallNoReducing ps = instantiateForallAux✝ ps 0 e

def Lean.Expr.instantiateForallNoReducingNoError (e : Expr) (ps : Array Expr) : Expr

Equations

• e.instantiateForallNoReducingNoError ps = instantiateForallAuxNoError✝ ps 0 e

def Lean.Meta.withoutMVarAssignments {α : Type} (m : MetaM α) : MetaM α

Equations

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

def Lean.Meta.inspectMVarAssignments : MetaM Unit

Equations

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

noncomputable def getInstanceFromLeftNonemptyFact {t : Sort u_1} (nonemptyFact : Nonempty t = True) : t

Equations

• getInstanceFromLeftNonemptyFact nonemptyFact = Classical.choice ⋯

noncomputable def getInstanceFromRightNonemptyFact {t : Sort u_1} (nonemptyFact : True = Nonempty t) : t

Equations

• getInstanceFromRightNonemptyFact nonemptyFact = Classical.choice ⋯

def getInstanceFromNonemptyFact (nonemptyFact : Lean.Expr) : Lean.MetaM Lean.Expr

Equations

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

def Lean.Meta.findInstance (ty : Expr) : MetaM (Option Expr)

Equations

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

def Lean.Meta.findInstance.simpleApply (lemmaProof goal : Expr) (fvars : Array Expr) : MetaM (Option Expr)

Equations

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

def Lean.Meta.findInstance.findInstanceForUninstantiatedMVars (prf : Expr) (fvars : Array Expr) : MetaM Bool

Equations

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

partial def getArity (e : Lean.Expr) : Nat

Returns the arity of e

def Lean.Meta.abstractAtExpr (e p : Expr) (occs : Occurrences := Occurrences.all) : MetaM Expr

Abstracts occurences of p in e. Previously, Meta.kabstract was used for this purpose, but because Meta.kabstract invokes definitional equality, there were some instances in which Meta.kabstract performed an abstraction at a position where RuleM.replace would not perform a replacement. This was an issue because it created inconsistencies between the clauses produced by superposition's main code and proof reconstruction.

abstractAtExpr is written to follow the implementation of Meta.kabstract without invoking definitional equality (instead testing for equality after instantiating metavariables).

Equations

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

def Lean.Meta.abstractAtExpr.visit (occs : Occurrences := Occurrences.all) (p : Expr) (pHeadIdx : HeadIndex) (pNumArgs : Nat) (e : Expr) (offset : Nat) : StateRefT' IO.RealWorld Nat MetaM Expr

Equations

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