Documentation

Std.Tactic.Ext.Attr

declare_ext_theorems_for A declares the extensionality theorems for the structure A.

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

Information about an extensionality theorem, stored in the environment extension.

Instances For
    Equations
    @[inline]

    Get the list of @[ext] lemmas corresponding to the key ty.

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

    Registers an extensionality lemma.

    When @[ext] is applied to a structure, it generates .ext and .ext_iff theorems and registers them for the ext tactic.

    When @[ext] is applied to a theorem, the theorem is registered for the ext tactic.

    You can use @[ext 9000] to specify a priority for the attribute.

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