structure Aesop.Slot : Type

A slot represents a maximal premise of a forward rule, i.e. a premise with no forward dependencies. The goal of forward reasoning is to assign a hypothesis to each slot in such a way that the assignments agree on all variables shared between them.

Exceptionally, a slot can also represent the rule pattern substitution. Rules with a rule pattern have exactly one such slot, which is assigned an arbitrary premise index.

• typeDiscrTreeKeys? : Option (Array Lean.Meta.DiscrTree.Key)

  Discrimination tree keys for the type of this slot. If the slot is for the rule pattern, it is not associated with a premise, so doesn't have discrimination tree keys.

• index : SlotIndex

  Index of the slot. Slots are always part of a list of slots, and index is the 0-based index of this slot in that list.

• premiseIndex : PremiseIndex

  0-based index of the premise represented by this slot in the rule type. Note that the slots array may use a different ordering than the original order of premises, so we don't always have index ≤ premiseIndex. Rule pattern slots are assigned an arbitrary premise index.

• deps : Std.HashSet PremiseIndex

  The previous premises that the premise of this slot depends on.

• common : Std.HashSet PremiseIndex

  Common variables shared between this slot and the previous slots.

• forwardDeps : Array PremiseIndex

  The forward dependencies of this slot. These are all the premises that appear in slots after this one.

@[implicit_reducible]

instance Aesop.instInhabitedSlot : Inhabited Slot

Equations

• Aesop.instInhabitedSlot = { default := Aesop.instInhabitedSlot.default }

def Aesop.instInhabitedSlot.default : Slot

Equations

• Aesop.instInhabitedSlot.default = { typeDiscrTreeKeys? := default, index := default, premiseIndex := default, deps := default, common := default, forwardDeps := default }

@[implicit_reducible]

def Aesop.instBEqSlot : BEq Slot

Equations

• Aesop.instBEqSlot = { beq := fun (s₁ s₂ : Aesop.Slot) => s₁.premiseIndex == s₂.premiseIndex }

@[implicit_reducible]

def Aesop.instHashableSlot : Hashable Slot

Equations

• Aesop.instHashableSlot = { hash := fun (x : Aesop.Slot) => hash x.premiseIndex }

structure Aesop.ForwardRuleInfo : Type

Information about the decomposed type of a forward rule.

• numPremises : Nat

  The rule's number of premises.

• numLevelParams : Nat

  The number of distinct level parameters and level metavariables occurring in the rule's type. We expect that these turn into level metavariables when the rule is elaborated.

• slotClusters : Array (Array Slot)

  Slots representing the maximal premises of the forward rule, partitioned into metavariable clusters.

• conclusionDeps : Array PremiseIndex

  The premises that appear in the rule's conclusion.

• rulePatternInfo? : Option (RulePattern × PremiseIndex)

  The rule's rule pattern and the premise index that was assigned to it.

@[implicit_reducible]

instance Aesop.instInhabitedForwardRuleInfo : Inhabited ForwardRuleInfo

Equations

• Aesop.instInhabitedForwardRuleInfo = { default := Aesop.instInhabitedForwardRuleInfo.default }

def Aesop.instInhabitedForwardRuleInfo.default : ForwardRuleInfo

Equations

• Aesop.instInhabitedForwardRuleInfo.default = { numPremises := default, numLevelParams := default, slotClusters := default, conclusionDeps := default, rulePatternInfo? := default }

def Aesop.ForwardRuleInfo.isConstant (r : ForwardRuleInfo) : Bool

Is this rule a constant rule (i.e., does it have neither premises nor a rule pattern)? Note: the rule may still have instance arguments.

Equations

• r.isConstant = (r.numPremises == 0 && r.rulePatternInfo?.isNone)

def Aesop.ForwardRuleInfo.ofExpr (thm : Lean.Expr) (rulePattern? : Option RulePattern) (immediate : UnorderedArraySet PremiseIndex) : Lean.MetaM ForwardRuleInfo

Construct a ForwardRuleInfo for the theorem thm.

Equations

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