@[inline]

def Lean.Meta.Grind.isSameExpr (a b : Expr) : Bool

Equations

• Lean.Meta.Grind.isSameExpr a b = Lean.Meta.Grind.isSameExpr.unsafe_impl_1 a b

def Lean.Meta.Grind.congrPlaceholderProof : Expr

We use this auxiliary constant to mark delayed congruence proofs.

Equations

• Lean.Meta.Grind.congrPlaceholderProof = Lean.mkConst (Lean.Name.mkSimple "[congruence]")

def Lean.Meta.Grind.isInterpreted (e : Expr) : MetaM Bool

Returns true if e is True, False, or a literal value. See LitValues for supported literals.

Equations

• Lean.Meta.Grind.isInterpreted e = if (e.isTrue || e.isFalse) = true then pure true else do let y ← pure PUnit.unit (fun (y : PUnit) => Lean.Meta.isLitValue e) y

opaque Lean.Meta.Grind.grind.debug : Lean.Option Bool

opaque Lean.Meta.Grind.grind.debug.proofs : Lean.Option Bool

structure Lean.Meta.Grind.Context : Type

Context for GrindM monad.

• simp : Simp.Context
• simprocs : Array Simprocs
• mainDeclName : Name
• config : Grind.Config

structure Lean.Meta.Grind.CongrTheoremCacheKey : Type

Key for the congruence theorem cache.

• f : Expr
• numArgs : Nat

instance Lean.Meta.Grind.instBEqCongrTheoremCacheKey : BEq CongrTheoremCacheKey

Equations

• Lean.Meta.Grind.instBEqCongrTheoremCacheKey = { beq := fun (a b : Lean.Meta.Grind.CongrTheoremCacheKey) => Lean.Meta.Grind.isSameExpr a.f b.f && a.numArgs == b.numArgs }

instance Lean.Meta.Grind.instHashableCongrTheoremCacheKey : Hashable CongrTheoremCacheKey

Equations

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

structure Lean.Meta.Grind.CoreState : Type

State for the GrindM monad.

• canon : Canon.State
• scState : ShareCommon.State ShareCommon.objectFactory

  ShareCommon (aka Hashconsing) state.

• nextThmIdx : Nat

  Next index for creating auxiliary theorems.

• congrThms : PHashMap CongrTheoremCacheKey CongrTheorem

  Congruence theorems generated so far. Recall that for constant symbols we rely on the reserved name feature (i.e., mkHCongrWithArityForConst?). Remark: we currently do not reuse congruence theorems

• simpStats : Simp.Stats
• trueExpr : Expr
• falseExpr : Expr

instance Lean.Meta.Grind.instNonemptyMethodsRef : Nonempty Lean.Meta.Grind.MethodsRef✝

@[reducible, inline]

abbrev Lean.Meta.Grind.GrindM (α : Type) : Type

Equations

• Lean.Meta.Grind.GrindM = ReaderT Lean.Meta.Grind.MethodsRef✝ (ReaderT Lean.Meta.Grind.Context (StateRefT' IO.RealWorld Lean.Meta.Grind.CoreState Lean.MetaM))

def Lean.Meta.Grind.getConfig : GrindM Grind.Config

Returns the user-defined configuration options

Equations

• Lean.Meta.Grind.getConfig = do let __do_lift ← readThe Lean.Meta.Grind.Context pure __do_lift.config

def Lean.Meta.Grind.getTrueExpr : GrindM Expr

Returns the internalized True constant.

Equations

• Lean.Meta.Grind.getTrueExpr = do let __do_lift ← get pure __do_lift.trueExpr

def Lean.Meta.Grind.getFalseExpr : GrindM Expr

Returns the internalized False constant.

Equations

• Lean.Meta.Grind.getFalseExpr = do let __do_lift ← get pure __do_lift.falseExpr

def Lean.Meta.Grind.getMainDeclName : GrindM Name

Equations

• Lean.Meta.Grind.getMainDeclName = do let __do_lift ← readThe Lean.Meta.Grind.Context pure __do_lift.mainDeclName

@[inline]

def Lean.Meta.Grind.getMethodsRef : GrindM Lean.Meta.Grind.MethodsRef✝

Equations

• Lean.Meta.Grind.getMethodsRef = read

def Lean.Meta.Grind.getMaxGeneration : GrindM Nat

Returns maximum term generation that is considered during ematching.

Equations

• Lean.Meta.Grind.getMaxGeneration = do let __do_lift ← Lean.Meta.Grind.getConfig pure __do_lift.gen

def Lean.Meta.Grind.abstractNestedProofs (e : Expr) : GrindM Expr

Abtracts nested proofs in e. This is a preprocessing step performed before internalization.

Equations

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

def Lean.Meta.Grind.shareCommon (e : Expr) : GrindM Expr

Applies hash-consing to e. Recall that all expressions in a grind goal have been hash-consing. We perform this step before we internalize expressions.

Equations

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

def Lean.Meta.Grind.canon (e : Expr) : GrindM Expr

Canonicalizes nested types, type formers, and instances in e.

Equations

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

def Lean.Meta.Grind.isTrueExpr (e : Expr) : GrindM Bool

Returns true if e is the internalized True expression.

Equations

• Lean.Meta.Grind.isTrueExpr e = do let __do_lift ← Lean.Meta.Grind.getTrueExpr pure (Lean.Meta.Grind.isSameExpr e __do_lift)

def Lean.Meta.Grind.isFalseExpr (e : Expr) : GrindM Bool

Returns true if e is the internalized False expression.

Equations

• Lean.Meta.Grind.isFalseExpr e = do let __do_lift ← Lean.Meta.Grind.getFalseExpr pure (Lean.Meta.Grind.isSameExpr e __do_lift)

def Lean.Meta.Grind.mkHCongrWithArity (f : Expr) (numArgs : Nat) : GrindM CongrTheorem

Creates a congruence theorem for a f-applications with numArgs arguments.

Equations

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

structure Lean.Meta.Grind.ENode : Type

Stores information for a node in the egraph. Each internalized expression e has an ENode associated with it.

• self : Expr

  Node represented by this ENode.

• next : Expr

  Next element in the equivalence class.

• root : Expr

  Root (aka canonical representative) of the equivalence class

• congr : Expr

  congr is the term self is congruent to. We say self is the congruence class root if isSameExpr congr self. This field is initialized to self even if e is not an application.

• target? : Option Expr

  When e was added to this equivalence class because of an equality h : e = target, then we store target here, and h at proof?.

• proof? : Option Expr
• flipped : Bool

  Proof has been flipped.

• size : Nat

  Number of elements in the equivalence class, this field is meaningless if node is not the root.

• interpreted : Bool

  interpreted := true if node should be viewed as an abstract value.

• ctor : Bool

  ctor := true if the head symbol is a constructor application.

• hasLambdas : Bool

  hasLambdas := true if equivalence class contains lambda expressions.

• heqProofs : Bool

  If heqProofs := true, then some proofs in the equivalence class are based on heterogeneous equality.

• idx : Nat

  Unique index used for pretty printing and debugging purposes.

• generation : Nat
• mt : Nat

  Modification time

instance Lean.Meta.Grind.instInhabitedENode : Inhabited ENode

Equations

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

instance Lean.Meta.Grind.instReprENode : Repr ENode

Equations

• Lean.Meta.Grind.instReprENode = { reprPrec := Lean.Meta.Grind.reprENode✝ }

def Lean.Meta.Grind.ENode.isCongrRoot (n : ENode) : Bool

Equations

• n.isCongrRoot = Lean.Meta.Grind.isSameExpr n.self n.congr

structure Lean.Meta.Grind.NewEq : Type

New equality to be processed.

• lhs : Expr
• rhs : Expr
• proof : Expr
• isHEq : Bool

instance Lean.Meta.Grind.instHashableENodeKey : Hashable Lean.Meta.Grind.ENodeKey✝

Equations

• Lean.Meta.Grind.instHashableENodeKey = { hash := fun (k : Lean.Meta.Grind.ENodeKey✝) => Lean.Meta.Grind.instHashableENodeKey.unsafe_impl_1 k }

instance Lean.Meta.Grind.instBEqENodeKey : BEq Lean.Meta.Grind.ENodeKey✝

Equations

• Lean.Meta.Grind.instBEqENodeKey = { beq := fun (k₁ k₂ : Lean.Meta.Grind.ENodeKey✝) => Lean.Meta.Grind.isSameExpr k₁.expr k₂.expr }

@[reducible, inline]

abbrev Lean.Meta.Grind.ENodeMap : Type

Equations

• Lean.Meta.Grind.ENodeMap = Lean.PHashMap Lean.Meta.Grind.ENodeKey✝ Lean.Meta.Grind.ENode

structure Lean.Meta.Grind.CongrKey (enodes : ENodeMap) : Type

Key for the congruence table. We need access to the enodes to be able to retrieve the equivalence class roots.

• e : Expr

def Lean.Meta.Grind.hasSameRoot (enodes : ENodeMap) (a b : Expr) : Bool

Equations

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

def Lean.Meta.Grind.congrHash (enodes : ENodeMap) (e : Expr) : UInt64

Equations

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

def Lean.Meta.Grind.congrHash.goEq (enodes : ENodeMap) (lhs rhs : Expr) : UInt64

Equations

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

def Lean.Meta.Grind.congrHash.go (enodes : ENodeMap) (e : Expr) (r : UInt64) : UInt64

Equations

• Lean.Meta.Grind.congrHash.go enodes (f.app a) r = Lean.Meta.Grind.congrHash.go enodes f (mixHash r (Lean.Meta.Grind.hashRoot✝ enodes a))
• Lean.Meta.Grind.congrHash.go enodes e r = mixHash r (Lean.Meta.Grind.hashRoot✝ enodes e)

def Lean.Meta.Grind.isCongruent (enodes : ENodeMap) (a b : Expr) : Bool

Returns true if a and b are congruent modulo the equivalence classes in enodes.

Equations

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

def Lean.Meta.Grind.isCongruent.goEq (enodes : ENodeMap) (lhs₁ rhs₁ lhs₂ rhs₂ : Expr) : Bool

Equations

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

partial def Lean.Meta.Grind.isCongruent.go (enodes : ENodeMap) (a b : Expr) : Bool

instance Lean.Meta.Grind.instHashableCongrKey {enodes : ENodeMap} : Hashable (CongrKey enodes)

Equations

• Lean.Meta.Grind.instHashableCongrKey = { hash := fun (k : Lean.Meta.Grind.CongrKey enodes) => Lean.Meta.Grind.congrHash enodes k.e }

instance Lean.Meta.Grind.instBEqCongrKey {enodes : ENodeMap} : BEq (CongrKey enodes)

Equations

• Lean.Meta.Grind.instBEqCongrKey = { beq := fun (k1 k2 : Lean.Meta.Grind.CongrKey enodes) => Lean.Meta.Grind.isCongruent enodes k1.e k2.e }

@[reducible, inline]

abbrev Lean.Meta.Grind.CongrTable (enodes : ENodeMap) : Type

Equations

• Lean.Meta.Grind.CongrTable enodes = Lean.PHashSet (Lean.Meta.Grind.CongrKey enodes)

@[reducible, inline]

abbrev Lean.Meta.Grind.ParentSet : Type

Equations

• Lean.Meta.Grind.ParentSet = Lean.RBTree Lean.Expr Lean.Expr.quickComp

@[reducible, inline]

abbrev Lean.Meta.Grind.ParentMap : Type

Equations

• Lean.Meta.Grind.ParentMap = Lean.PHashMap Lean.Meta.Grind.ENodeKey✝ Lean.Meta.Grind.ParentSet

structure Lean.Meta.Grind.PreInstance : Type

The E-matching module instantiates theorems using the EMatchTheorem proof and a (partial) assignment. We want to avoid instantiating the same theorem with the same assignment more than once. Therefore, we store the (pre-)instance information in set. Recall that the proofs of activated theorems have been hash-consed. The assignment contains internalized expressions, which have also been hash-consed.

• proof : Expr
• assignment : Array Expr

instance Lean.Meta.Grind.instHashablePreInstance : Hashable PreInstance

Equations

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

instance Lean.Meta.Grind.instBEqPreInstance : BEq PreInstance

Equations

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

@[reducible, inline]

abbrev Lean.Meta.Grind.PreInstanceSet : Type

Equations

• Lean.Meta.Grind.PreInstanceSet = Lean.PHashSet Lean.Meta.Grind.PreInstance

structure Lean.Meta.Grind.NewFact : Type

New fact to be processed.

• proof : Expr
• prop : Expr
• generation : Nat

instance Lean.Meta.Grind.instInhabitedNewFact : Inhabited NewFact

Equations

• Lean.Meta.Grind.instInhabitedNewFact = { default := { proof := default, prop := default, generation := default } }

structure Lean.Meta.Grind.Goal : Type

• mvarId : MVarId
• enodes : ENodeMap
• parents : ParentMap
• congrTable : CongrTable self.enodes
• appMap : PHashMap HeadIndex (List Expr)

  A mapping from each function application index (HeadIndex) to a list of applications with that index. Recall that the HeadIndex for a constant is its constant name, and for a free variable, it is its unique id.

• newEqs : Array NewEq

  Equations to be processed.

• inconsistent : Bool

  inconsistent := true if ENodes for True and False are in the same equivalence class.

• gmt : Nat

  Goal modification time.

• nextIdx : Nat

  Next unique index for creating ENodes

• thms : PArray EMatchTheorem

  Active theorems that we have performed ematching at least once.

• newThms : PArray EMatchTheorem

  Active theorems that we have not performed any round of ematching yet.

• thmMap : EMatchTheorems

  Inactive global theorems. As we internalize terms, we activate theorems as we find their symbols. Local theorem provided by users are added directly into newThms.

• numInstances : Nat

  Number of theorem instances generated so far

• preInstances : PreInstanceSet

  (pre-)instances found so far. It includes instances that failed to be instantiated.

• newFacts : Std.Queue NewFact

  new facts to be processed.

instance Lean.Meta.Grind.instInhabitedGoal : Inhabited Goal

Equations

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

def Lean.Meta.Grind.Goal.admit (goal : Goal) : MetaM Unit

Equations

• goal.admit = goal.mvarId.admit

@[reducible, inline]

abbrev Lean.Meta.Grind.GoalM (α : Type) : Type

Equations

• Lean.Meta.Grind.GoalM = StateRefT' IO.RealWorld Lean.Meta.Grind.Goal Lean.Meta.Grind.GrindM

@[inline]

def Lean.Meta.Grind.GoalM.run {α : Type} (goal : Goal) (x : GoalM α) : GrindM (α × Goal)

Equations

• Lean.Meta.Grind.GoalM.run goal x = goal.mvarId.withContext (StateRefT'.run x goal)

@[inline]

def Lean.Meta.Grind.GoalM.run' (goal : Goal) (x : GoalM Unit) : GrindM Goal

Equations

• Lean.Meta.Grind.GoalM.run' goal x = goal.mvarId.withContext ((x *> get).run' goal)

def Lean.Meta.Grind.markTheoremInstance (proof : Expr) (assignment : Array Expr) : GoalM Bool

A helper function used to mark a theorem instance found by the E-matching module. It returns true if it is a new instance and false otherwise.

Equations

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

def Lean.Meta.Grind.addNewFact (proof prop : Expr) (generation : Nat) : GoalM Unit

Adds a new fact prop with proof proof to the queue for processing.

Equations

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

def Lean.Meta.Grind.addTheoremInstance (proof prop : Expr) (generation : Nat) : GoalM Unit

Adds a new theorem instance produced using E-matching.

Equations

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

def Lean.Meta.Grind.checkMaxInstancesExceeded : GoalM Bool

Returns true if the maximum number of instances has been reached.

Equations

• Lean.Meta.Grind.checkMaxInstancesExceeded = do let __do_lift ← get let __do_lift_1 ← liftM Lean.Meta.Grind.getConfig pure (decide (__do_lift.numInstances ≥ __do_lift_1.instances))

def Lean.Meta.Grind.getENode? (e : Expr) : GoalM (Option ENode)

Returns some n if e has already been "internalized" into the Otherwise, returns nones.

Equations

• Lean.Meta.Grind.getENode? e = do let __do_lift ← get pure (Lean.PersistentHashMap.find? __do_lift.enodes { expr := e })

def Lean.Meta.Grind.getENode (e : Expr) : GoalM ENode

Returns node associated with e. It assumes e has already been internalized.

Equations

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

def Lean.Meta.Grind.getGeneration (e : Expr) : GoalM Nat

Returns the generation of the given term. Is assumes it has been internalized

Equations

• Lean.Meta.Grind.getGeneration e = do let __do_lift ← Lean.Meta.Grind.getENode e pure __do_lift.generation

def Lean.Meta.Grind.isEqTrue (e : Expr) : GoalM Bool

Returns true if e is in the equivalence class of True.

Equations

• Lean.Meta.Grind.isEqTrue e = do let n ← Lean.Meta.Grind.getENode e let __do_lift ← liftM Lean.Meta.Grind.getTrueExpr pure (Lean.Meta.Grind.isSameExpr n.root __do_lift)

def Lean.Meta.Grind.isEqFalse (e : Expr) : GoalM Bool

Returns true if e is in the equivalence class of False.

Equations

• Lean.Meta.Grind.isEqFalse e = do let n ← Lean.Meta.Grind.getENode e let __do_lift ← liftM Lean.Meta.Grind.getFalseExpr pure (Lean.Meta.Grind.isSameExpr n.root __do_lift)

def Lean.Meta.Grind.isEqv (a b : Expr) : GoalM Bool

Returns true if a and b are in the same equivalence class.

Equations

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

def Lean.Meta.Grind.isRoot (e : Expr) : GoalM Bool

Returns true if the root of its equivalence class.

Equations

• Lean.Meta.Grind.isRoot e = do let __discr ← Lean.Meta.Grind.getENode? e match __discr with | some n => pure (Lean.Meta.Grind.isSameExpr n.root e) | x => pure false

def Lean.Meta.Grind.getRoot? (e : Expr) : GoalM (Option Expr)

Returns the root element in the equivalence class of e IF e has been internalized.

Equations

• Lean.Meta.Grind.getRoot? e = do let __discr ← Lean.Meta.Grind.getENode? e match __discr with | some n => pure (some n.root) | x => pure none

def Lean.Meta.Grind.getRoot (e : Expr) : GoalM Expr

Returns the root element in the equivalence class of e.

Equations

• Lean.Meta.Grind.getRoot e = do let __do_lift ← Lean.Meta.Grind.getENode e pure __do_lift.root

def Lean.Meta.Grind.getRootENode (e : Expr) : GoalM ENode

Returns the root enode in the equivalence class of e.

Equations

• Lean.Meta.Grind.getRootENode e = do let __do_lift ← Lean.Meta.Grind.getRoot e Lean.Meta.Grind.getENode __do_lift

def Lean.Meta.Grind.getNext (e : Expr) : GoalM Expr

Returns the next element in the equivalence class of e.

Equations

• Lean.Meta.Grind.getNext e = do let __do_lift ← Lean.Meta.Grind.getENode e pure __do_lift.next

def Lean.Meta.Grind.alreadyInternalized (e : Expr) : GoalM Bool

Returns true if e has already been internalized.

Equations

• Lean.Meta.Grind.alreadyInternalized e = do let __do_lift ← get pure (Lean.PersistentHashMap.contains __do_lift.enodes { expr := e })

def Lean.Meta.Grind.getTarget? (e : Expr) : GoalM (Option Expr)

Equations

• Lean.Meta.Grind.getTarget? e = do let __discr ← Lean.Meta.Grind.getENode? e match __discr with | some n => pure n.target? | x => pure none

def Lean.Meta.Grind.pushEqCore (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit

If isHEq is false, it pushes lhs = rhs with proof to newEqs. Otherwise, it pushes HEq lhs rhs.

Equations

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

def Lean.Meta.Grind.hasSameType (a b : Expr) : MetaM Bool

Return true if a and b have the same type.

Equations

• Lean.Meta.Grind.hasSameType a b = Lean.Meta.withDefault do let __do_lift ← Lean.Meta.inferType a let __do_lift_1 ← Lean.Meta.inferType b Lean.Meta.isDefEq __do_lift __do_lift_1

@[inline]

def Lean.Meta.Grind.pushEqHEq (lhs rhs proof : Expr) : GoalM Unit

Equations

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

@[inline]

def Lean.Meta.Grind.pushEq (lhs rhs proof : Expr) : GoalM Unit

Pushes lhs = rhs with proof to newEqs.

Equations

• Lean.Meta.Grind.pushEq lhs rhs proof = Lean.Meta.Grind.pushEqCore lhs rhs proof false

@[inline]

def Lean.Meta.Grind.pushHEq (lhs rhs proof : Expr) : GoalM Unit

Pushes HEq lhs rhs with proof to newEqs.

Equations

• Lean.Meta.Grind.pushHEq lhs rhs proof = Lean.Meta.Grind.pushEqCore lhs rhs proof true

def Lean.Meta.Grind.pushEqTrue (a proof : Expr) : GoalM Unit

Pushes a = True with proof to newEqs.

Equations

• Lean.Meta.Grind.pushEqTrue a proof = do let __do_lift ← liftM Lean.Meta.Grind.getTrueExpr Lean.Meta.Grind.pushEq a __do_lift proof

def Lean.Meta.Grind.pushEqFalse (a proof : Expr) : GoalM Unit

Pushes a = False with proof to newEqs.

Equations

• Lean.Meta.Grind.pushEqFalse a proof = do let __do_lift ← liftM Lean.Meta.Grind.getFalseExpr Lean.Meta.Grind.pushEq a __do_lift proof

def Lean.Meta.Grind.registerParent (parent child : Expr) : GoalM Unit

Records that parent is a parent of child. This function actually stores the information in the root (aka canonical representative) of child.

Equations

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

def Lean.Meta.Grind.getParents (e : Expr) : GoalM ParentSet

Returns the set of expressions e is a child of, or an expression in es equivalence class is a child of. The information is only up to date if e is the root (aka canonical representative) of the equivalence class.

Equations

• Lean.Meta.Grind.getParents e = do let __do_lift ← get match Lean.PersistentHashMap.find? __do_lift.parents { expr := e } with | some parents => pure parents | x => pure ∅

def Lean.Meta.Grind.getParentsAndReset (e : Expr) : GoalM ParentSet

Similar to getParents, but also removes the entry e ↦ parents from the parent map.

Equations

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

def Lean.Meta.Grind.copyParentsTo (parents : ParentSet) (root : Expr) : GoalM Unit

Copy parents to the parents of root. root must be the root of its equivalence class.

Equations

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

def Lean.Meta.Grind.setENode (e : Expr) (n : ENode) : GoalM Unit

Equations

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

def Lean.Meta.Grind.mkENodeCore (e : Expr) (interpreted ctor : Bool) (generation : Nat) : GoalM Unit

Equations

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

def Lean.Meta.Grind.mkENode (e : Expr) (generation : Nat) : GoalM Unit

Creates an ENode for e if one does not already exist. This method assumes e has been hashconsed.

Equations

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

def Lean.Meta.Grind.isCongrRoot (e : Expr) : GoalM Bool

Returns true is e is the root of its congruence class.

Equations

• Lean.Meta.Grind.isCongrRoot e = do let __do_lift ← Lean.Meta.Grind.getENode e pure __do_lift.isCongrRoot

partial def Lean.Meta.Grind.getCongrRoot (e : Expr) : GoalM Expr

Returns the root of the congruence class containing e.

def Lean.Meta.Grind.isInconsistent : GoalM Bool

Return true if the goal is inconsistent.

Equations

• Lean.Meta.Grind.isInconsistent = do let __do_lift ← get pure __do_lift.inconsistent

@[extern lean_grind_mk_eq_proof]

opaque Lean.Meta.Grind.mkEqProof (a b : Expr) : GoalM Expr

Returns a proof that a = b. It assumes a and b are in the same equivalence class, and have the same type.

@[extern lean_grind_mk_heq_proof]

opaque Lean.Meta.Grind.mkHEqProof (a b : Expr) : GoalM Expr

Returns a proof that HEq a b. It assumes a and b are in the same equivalence class.

def Lean.Meta.Grind.mkEqHEqProof (a b : Expr) : GoalM Expr

Returns a proof that a = b if they have the same type. Otherwise, returns a proof of HEq a b. It assumes a and b are in the same equivalence class.

Equations

• Lean.Meta.Grind.mkEqHEqProof a b = do let __do_lift ← liftM (Lean.Meta.Grind.hasSameType a b) if __do_lift = true then Lean.Meta.Grind.mkEqProof a b else Lean.Meta.Grind.mkHEqProof a b

def Lean.Meta.Grind.mkEqTrueProof (a : Expr) : GoalM Expr

Returns a proof that a = True. It assumes a and True are in the same equivalence class.

Equations

• Lean.Meta.Grind.mkEqTrueProof a = do let __do_lift ← liftM Lean.Meta.Grind.getTrueExpr Lean.Meta.Grind.mkEqProof a __do_lift

def Lean.Meta.Grind.mkEqFalseProof (a : Expr) : GoalM Expr

Returns a proof that a = False. It assumes a and False are in the same equivalence class.

Equations

• Lean.Meta.Grind.mkEqFalseProof a = do let __do_lift ← liftM Lean.Meta.Grind.getFalseExpr Lean.Meta.Grind.mkEqProof a __do_lift

def Lean.Meta.Grind.markAsInconsistent : GoalM Unit

Marks current goal as inconsistent without assigning mvarId.

Equations

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

def Lean.Meta.Grind.closeGoal (falseProof : Expr) : GoalM Unit

Closes the current goal using the given proof of False and marks it as inconsistent if it is not already marked so.

Equations

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

def Lean.Meta.Grind.getENodes : GoalM (Array ENode)

Returns all enodes in the goal

Equations

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

def Lean.Meta.Grind.forEachENode (f : ENode → GoalM Unit) : GoalM Unit

Equations

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

def Lean.Meta.Grind.filterENodes (p : ENode → GoalM Bool) : GoalM (Array ENode)

Equations

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

def Lean.Meta.Grind.forEachEqc (f : ENode → GoalM Unit) : GoalM Unit

Equations

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

@[reducible, inline]

abbrev Lean.Meta.Grind.Propagator : Type

Equations

• Lean.Meta.Grind.Propagator = (Lean.Expr → Lean.Meta.Grind.GoalM Unit)

@[reducible, inline]

abbrev Lean.Meta.Grind.Fallback : Type

Equations

• Lean.Meta.Grind.Fallback = Lean.Meta.Grind.GoalM Unit

structure Lean.Meta.Grind.Methods : Type

• propagateUp : Propagator
• propagateDown : Propagator
• fallback : Fallback

instance Lean.Meta.Grind.instInhabitedMethods : Inhabited Methods

Equations

• Lean.Meta.Grind.instInhabitedMethods = { default := { propagateUp := default, propagateDown := default, fallback := default } }

def Lean.Meta.Grind.Methods.toMethodsRef (m : Methods) : Lean.Meta.Grind.MethodsRef✝

Equations

• m.toMethodsRef = Lean.Meta.Grind.Methods.toMethodsRef.unsafe_impl_1 m

@[inline]

def Lean.Meta.Grind.getMethods : GrindM Methods

Equations

• Lean.Meta.Grind.getMethods = do let __do_lift ← Lean.Meta.Grind.getMethodsRef pure __do_lift.toMethods

def Lean.Meta.Grind.propagateUp (e : Expr) : GoalM Unit

Equations

• Lean.Meta.Grind.propagateUp e = do let __do_lift ← liftM Lean.Meta.Grind.getMethods __do_lift.propagateUp e

def Lean.Meta.Grind.propagateDown (e : Expr) : GoalM Unit

Equations

• Lean.Meta.Grind.propagateDown e = do let __do_lift ← liftM Lean.Meta.Grind.getMethods __do_lift.propagateDown e

def Lean.Meta.Grind.applyFallback : GoalM Unit

Equations

• Lean.Meta.Grind.applyFallback = do let __do_lift ← liftM Lean.Meta.Grind.getMethods let fallback : Lean.Meta.Grind.GoalM Unit := __do_lift.fallback fallback

def Lean.Meta.Grind.getEqc (e : Expr) : GoalM (List Expr)

Returns expressions in the given expression equivalence class.

Equations

• Lean.Meta.Grind.getEqc e = Lean.Meta.Grind.getEqc.go e e []

partial def Lean.Meta.Grind.getEqc.go (first e : Expr) (acc : List Expr) : GoalM (List Expr)

def Lean.Meta.Grind.getEqcs : GoalM (List (List Expr))

Returns all equivalence classes in the current goal.

Equations

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