Documentation

Aesop.Forward.RuleInfo

structure Aesop.Slot :

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 indexpremiseIndex. Rule pattern slots are assigned an arbitrary premise index.

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

  • 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
    Equations
      Instances For
        Equations
          Instances For

            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

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

              Equations
                Instances For

                  Construct a ForwardRuleInfo for the theorem thm.

                  Equations
                    Instances For

                      Sort slots such that each slot has at least one variable in common with the previous slots.

                      Equations
                        Instances For