@[inline]

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

Equations

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

def Lean.Meta.Grind.congrPlaceholderProof : Lean.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 : Lean.Expr) : Lean.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 : Lean.Meta.Simp.Context
• simprocs : Array Lean.Meta.Simprocs
• mainDeclName : Lean.Name
• config : Lean.Grind.Config

structure Lean.Meta.Grind.CongrTheoremCacheKey : Type

Key for the congruence theorem cache.

• f : Lean.Expr
• numArgs : Nat

Instances For

• Lean.Meta.Grind.instBEqCongrTheoremCacheKey
• Lean.Meta.Grind.instHashableCongrTheoremCacheKey

instance Lean.Meta.Grind.instBEqCongrTheoremCacheKey : BEq Lean.Meta.Grind.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 Lean.Meta.Grind.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 : Lean.Meta.Grind.Canon.State
• scState : ShareCommon.State Lean.ShareCommon.objectFactory

  ShareCommon (aka Hashconsing) state.

• nextThmIdx : Nat

  Next index for creating auxiliary theorems.

• congrThms : Lean.PHashMap Lean.Meta.Grind.CongrTheoremCacheKey Lean.Meta.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 : Lean.Meta.Simp.Stats
• trueExpr : Lean.Expr
• falseExpr : Lean.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 : Lean.Meta.Grind.GrindM Lean.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 : Lean.Meta.Grind.GrindM Lean.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 : Lean.Meta.Grind.GrindM Lean.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 : Lean.Meta.Grind.GrindM Lean.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 : Lean.Meta.Grind.GrindM Lean.Meta.Grind.MethodsRef✝

Equations

• Lean.Meta.Grind.getMethodsRef = read

def Lean.Meta.Grind.getMaxGeneration : Lean.Meta.Grind.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 : Lean.Expr) : Lean.Meta.Grind.GrindM Lean.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 : Lean.Expr) : Lean.Meta.Grind.GrindM Lean.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 : Lean.Expr) : Lean.Meta.Grind.GrindM Lean.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 : Lean.Expr) : Lean.Meta.Grind.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 : Lean.Expr) : Lean.Meta.Grind.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 : Lean.Expr) (numArgs : Nat) : Lean.Meta.Grind.GrindM Lean.Meta.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 : Lean.Expr

  Node represented by this ENode.

• next : Lean.Expr

  Next element in the equivalence class.

• root : Lean.Expr

  Root (aka canonical representative) of the equivalence class

• congr : Lean.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 Lean.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 Lean.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

Instances For

• Lean.Meta.Grind.instInhabitedENode
• Lean.Meta.Grind.instReprENode

instance Lean.Meta.Grind.instInhabitedENode : Inhabited Lean.Meta.Grind.ENode

Equations

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

instance Lean.Meta.Grind.instReprENode : Repr Lean.Meta.Grind.ENode

Equations

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

def Lean.Meta.Grind.ENode.isCongrRoot (n : Lean.Meta.Grind.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 : Lean.Expr
• rhs : Lean.Expr
• proof : Lean.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 : Lean.Meta.Grind.ENodeMap) : Type

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

• e : Lean.Expr

Instances For

• Lean.Meta.Grind.instBEqCongrKey
• Lean.Meta.Grind.instHashableCongrKey

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.Meta.Grind.congrHash.go (enodes : Lean.Meta.Grind.ENodeMap) (e : Lean.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 : Lean.Meta.Grind.ENodeMap) (a b : Lean.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 : Lean.Meta.Grind.ENodeMap) (lhs₁ rhs₁ lhs₂ rhs₂ : Lean.Expr) : Bool

Equations

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

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

instance Lean.Meta.Grind.instHashableCongrKey {enodes : Lean.Meta.Grind.ENodeMap} : Hashable (Lean.Meta.Grind.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 : Lean.Meta.Grind.ENodeMap} : BEq (Lean.Meta.Grind.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 : Lean.Meta.Grind.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 : Lean.Expr
• assignment : Array Lean.Expr

Instances For

• Lean.Meta.Grind.instBEqPreInstance
• Lean.Meta.Grind.instHashablePreInstance

instance Lean.Meta.Grind.instHashablePreInstance : Hashable Lean.Meta.Grind.PreInstance

Equations

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

instance Lean.Meta.Grind.instBEqPreInstance : BEq Lean.Meta.Grind.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 : Lean.Expr
• prop : Lean.Expr
• generation : Nat

Instances For

• Lean.Meta.Grind.instInhabitedNewFact

instance Lean.Meta.Grind.instInhabitedNewFact : Inhabited Lean.Meta.Grind.NewFact

Equations

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

structure Lean.Meta.Grind.Goal : Type

• mvarId : Lean.MVarId
• enodes : Lean.Meta.Grind.ENodeMap
• parents : Lean.Meta.Grind.ParentMap
• congrTable : Lean.Meta.Grind.CongrTable self.enodes
• appMap : Lean.PHashMap Lean.HeadIndex (List Lean.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 Lean.Meta.Grind.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 : Lean.PArray Lean.Meta.Grind.EMatchTheorem

  Active theorems that we have performed ematching at least once.

• newThms : Lean.PArray Lean.Meta.Grind.EMatchTheorem

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

• thmMap : Lean.Meta.Grind.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 : Lean.Meta.Grind.PreInstanceSet

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

• newFacts : Std.Queue Lean.Meta.Grind.NewFact

  new facts to be processed.

Instances For

• Lean.Meta.Grind.instInhabitedGoal

instance Lean.Meta.Grind.instInhabitedGoal : Inhabited Lean.Meta.Grind.Goal

Equations

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

def Lean.Meta.Grind.Goal.admit (goal : Lean.Meta.Grind.Goal) : Lean.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 : Lean.Meta.Grind.Goal) (x : Lean.Meta.Grind.GoalM α) : Lean.Meta.Grind.GrindM (α × Lean.Meta.Grind.Goal)

Equations

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

@[inline]

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

Equations

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

def Lean.Meta.Grind.markTheoremInstance (proof : Lean.Expr) (assignment : Array Lean.Expr) : Lean.Meta.Grind.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 : Lean.Expr) (generation : Nat) : Lean.Meta.Grind.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 : Lean.Expr) (generation : Nat) : Lean.Meta.Grind.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 : Lean.Meta.Grind.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 : Lean.Expr) : Lean.Meta.Grind.GoalM (Option Lean.Meta.Grind.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 : Lean.Expr) : Lean.Meta.Grind.GoalM Lean.Meta.Grind.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 : Lean.Expr) : Lean.Meta.Grind.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 : Lean.Expr) : Lean.Meta.Grind.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 : Lean.Expr) : Lean.Meta.Grind.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 : Lean.Expr) : Lean.Meta.Grind.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 : Lean.Expr) : Lean.Meta.Grind.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 : Lean.Expr) : Lean.Meta.Grind.GoalM (Option Lean.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 : Lean.Expr) : Lean.Meta.Grind.GoalM Lean.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 : Lean.Expr) : Lean.Meta.Grind.GoalM Lean.Meta.Grind.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 : Lean.Expr) : Lean.Meta.Grind.GoalM Lean.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 : Lean.Expr) : Lean.Meta.Grind.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 : Lean.Expr) : Lean.Meta.Grind.GoalM (Option Lean.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 : Lean.Expr) (isHEq : Bool) : Lean.Meta.Grind.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 : Lean.Expr) : Lean.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 : Lean.Expr) : Lean.Meta.Grind.GoalM Unit

Equations

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

@[inline]

def Lean.Meta.Grind.pushEq (lhs rhs proof : Lean.Expr) : Lean.Meta.Grind.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 : Lean.Expr) : Lean.Meta.Grind.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 : Lean.Expr) : Lean.Meta.Grind.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 : Lean.Expr) : Lean.Meta.Grind.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 : Lean.Expr) : Lean.Meta.Grind.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 : Lean.Expr) : Lean.Meta.Grind.GoalM Lean.Meta.Grind.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 : Lean.Expr) : Lean.Meta.Grind.GoalM Lean.Meta.Grind.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 : Lean.Meta.Grind.ParentSet) (root : Lean.Expr) : Lean.Meta.Grind.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 : Lean.Expr) (n : Lean.Meta.Grind.ENode) : Lean.Meta.Grind.GoalM Unit

Equations

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

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

Equations

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

def Lean.Meta.Grind.mkENode (e : Lean.Expr) (generation : Nat) : Lean.Meta.Grind.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 : Lean.Expr) : Lean.Meta.Grind.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 : Lean.Expr) : Lean.Meta.Grind.GoalM Lean.Expr

Returns the root of the congruence class containing e.

def Lean.Meta.Grind.isInconsistent : Lean.Meta.Grind.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 : Lean.Expr) : Lean.Meta.Grind.GoalM Lean.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 : Lean.Expr) : Lean.Meta.Grind.GoalM Lean.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 : Lean.Expr) : Lean.Meta.Grind.GoalM Lean.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 : Lean.Expr) : Lean.Meta.Grind.GoalM Lean.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 : Lean.Expr) : Lean.Meta.Grind.GoalM Lean.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 : Lean.Meta.Grind.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 : Lean.Expr) : Lean.Meta.Grind.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 : Lean.Meta.Grind.GoalM (Array Lean.Meta.Grind.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 : Lean.Meta.Grind.ENode → Lean.Meta.Grind.GoalM Unit) : Lean.Meta.Grind.GoalM Unit

Equations

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

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

Equations

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

def Lean.Meta.Grind.forEachEqc (f : Lean.Meta.Grind.ENode → Lean.Meta.Grind.GoalM Unit) : Lean.Meta.Grind.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 : Lean.Meta.Grind.Propagator
• propagateDown : Lean.Meta.Grind.Propagator
• fallback : Lean.Meta.Grind.Fallback

Instances For

• Lean.Meta.Grind.instInhabitedMethods

instance Lean.Meta.Grind.instInhabitedMethods : Inhabited Lean.Meta.Grind.Methods

Equations

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

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

Equations

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

@[inline]

def Lean.Meta.Grind.getMethods : Lean.Meta.Grind.GrindM Lean.Meta.Grind.Methods

Equations

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

def Lean.Meta.Grind.propagateUp (e : Lean.Expr) : Lean.Meta.Grind.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 : Lean.Expr) : Lean.Meta.Grind.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 : Lean.Meta.Grind.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 : Lean.Expr) : Lean.Meta.Grind.GoalM (List Lean.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 : Lean.Expr) (acc : List Lean.Expr) : Lean.Meta.Grind.GoalM (List Lean.Expr)

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

Returns all equivalence classes in the current goal.

Equations

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