source
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.

Instances For

source
instance Aesop.instInhabitedSlot :
Inhabited Slot
Equations

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

source
def Aesop.instInhabitedSlot.default :
Slot
Equations

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

Instances For

source
def Aesop.instBEqSlot :
BEq Slot
Equations

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

Instances For

source
def Aesop.instHashableSlot :
Hashable Slot
Equations

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

Instances For

source
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.

Instances For

source
instance Aesop.instInhabitedForwardRuleInfo :
Inhabited ForwardRuleInfo
Equations

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

source
def Aesop.instInhabitedForwardRuleInfo.default :
ForwardRuleInfo
Equations

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

Instances For

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

Is this rule a constant rule (i.e., does it have neither premises nor a rule pattern)?

Equations

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

Instances For

source
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.

Instances For