BeHOLd.ClassicalHOL.Equality (behold v1.1.3)

View Source

Provides various terms constructors as macros for different notions of equality. This includes variants of Leibniz equality, Andrews equality and extensional equality.

Summary

Functions

andrews_equality(type)

Constructor for Andrews equality on the given type, which defines equality by stating that both arguments share all reflexive relations. Generates an abstraction which can be applied to two arguments.

extensional_equality(type)

Constructor for extensional equality on the given function type, which defines equality by equality of the extensions. Generates an abstraction which can be applied to two arguments.

leibniz_equality(type, connective \\ equivalent_term())

Constructor for Leibniz equality on the given type, which defines equality by stating that both arguments share the same properties. Generates an abstraction which can be applied to two arguments.

Functions

andrews_equality(type)

@spec andrews_equality(HOL.Data.type()) :: HOL.Data.hol_term()

Constructor for Andrews equality on the given type, which defines equality by stating that both arguments share all reflexive relations. Generates an abstraction which can be applied to two arguments.

Example

iex> andrews_equality(type_i()) == parse("^[X:$i, Y:$i]: ![Q:$i>$i>$o] ((![Z:$i]: Q @ Z @ Z) => Q @ X @ Y)")
true

extensional_equality(type)

@spec extensional_equality(HOL.Data.type()) :: HOL.Data.hol_term()

Constructor for extensional equality on the given function type, which defines equality by equality of the extensions. Generates an abstraction which can be applied to two arguments.

Example

iex> extensional_equality(type_ii()) == parse("^[X:$i>i, Y:$i>i]: ![Z:$i]: X @ Z = Y @ Z")
true

leibniz_equality(type, connective \\ equivalent_term())

@spec leibniz_equality(HOL.Data.type(), HOL.Data.hol_term()) :: HOL.Data.hol_term()

Constructor for Leibniz equality on the given type, which defines equality by stating that both arguments share the same properties. Generates an abstraction which can be applied to two arguments.

Examples

iex> leibniz_equality(type_i(), equivalent_term()) == parse("^[X:$i, Y:$i]: ![P:$i>$o]: P @ X <=> P @ Y")
true

iex> leibniz_equality(type_i(), implied_by_term()) == parse("^[X:$i, Y:$i]: ![P:$i>$o]: P @ X <= P @ Y")
true