Documentation

Std.Tactic.CoeExt

The different types of coercions that are supported by the coe attribute.

Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    • The number of arguments to the coercion function

      numArgs : Nat
    • The argument index that represents the value being coerced

      coercee : Nat
    • The type of coercion

    Information associated to a coercion function to enable sensible delaboration.

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

      The environment extension for tracking coercion functions for delaboration

      Lookup the coercion information for a given function

      Equations

      This delaborator tries to elide functions which are known coercions. For example, Int.ofNat is a coercion, so instead of printing ofNat n we just print ↑n↑n, and when re-parsing this we can (usually) recover the specific coercion being used.

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

      Add a coercion delaborator for the given function.

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

      Add name to the coercion extension and add a coercion delaborator for the function.

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

      The @[coe] attribute on a function (which should also appear in a instance : Coe A B := ⟨myFn⟩ declaration) allows the delaborator to show applications of this function as ↑↑ when printing expressions.

      Equations