Module prop::avatar_extensions
source[−]Expand description
Avatar Extensions
Avatar Extensions introduces avatars which are ways to wrap or unwrap propositions.
For more information, see https://advancedresearch.github.io/avatar-extensions/summary.html
Structs
Traits
Implemented by avatars.
Implememnted by commutative products.
Implemented by contravariant products.
Loop Witness.
Implemented by avatars that have their “clothes off”.
Implemented by products.
Implemented by avatars that have their “clothes on”.
Functions
a ∧ b => -(a * b) = (-a) * b
.
a ∧ b => -(a * b) = a * (-b)
.
Gets a loop witness from product witness.