Documentation

Aesop.Forward.Substitution

A substitution for the premises of a rule. Given a rule with type ∀ (x₁ : T₁) ... (xₙ : Tₙ), U a substitution is a finite partial map with domain {1, ..., n} that associates an expression with some or all of the premises.

  • premises : Array (Option RPINF)

    The substitution.

  • The level substitution implied by the premise substitution. If e is the elaborated rule expression (with level params replaced by level mvars), and collectLevelMVars (← instantiateMVars e) = [?m₁, ..., ?mₙ], then levels[i] is the level assigned to ?mᵢ.

Instances For
    def Aesop.Substitution.empty (numPremises numLevels : Nat) :

    The empty substitution for a rule with the given number of premise indexes.

    Equations
      Instances For

        Insert the mapping pi ↦ inst into the substitution s. Precondition: pi is in the domain of s.

        Equations
          Instances For

            Get the instantiation associated with premise pi in s. Precondition: pi is in the domain of s.

            Equations
              Instances For

                Insert the mapping li ↦ inst into the substitution s. Precondition: li is in the domain of s and inst is normalised.

                Equations
                  Instances For

                    Get the instantiation associated with level li in s. Precondition: li is in the domain of s.

                    Equations
                      Instances For

                        Merge two substitutions. Precondition: the substitutions are compatible, so they must have the same size and if s₁[x] and s₂[x] are both defined, they must be the same value.

                        Equations
                          Instances For

                            Returns true if any expression in the codomain of s contains hyp.

                            Equations
                              Instances For

                                Given e with type ∀ (x₁ : T₁) ... (xₙ : Tₙ), U and a substitution σ for the arguments xᵢ, replace occurrences of xᵢ in the body U with fresh metavariables (like forallMetaTelescope). Then, for each mapping xᵢ ↦ tᵢ in σ, assign tᵢ to the metavariable corresponding to xᵢ. Returns the newly created metavariables (which may be assigned!), their binder infos and the updated body.

                                Equations
                                  Instances For

                                    Given rule of type ∀ (x₁ : T₁) ... (xₙ : Tₙ), U and a substitution σ for the arguments xᵢ, specialise rule with the arguments given by σ. That is, construct U t₁ ... tₙ where tⱼ is σ(xⱼ) if xⱼ ∈ dom(σ) and is otherwise a fresh fvar, then λ-abstract the fresh fvars.

                                    Equations
                                      Instances For

                                        Open the type of a rule e. If a substitution σ is given, this function acts like Substitution.openRuleType σ. Otherwise it acts like forallMetaTelescope.

                                        Equations
                                          Instances For