Module prop::avatar_extensions

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

AntiMul

An anti-commutative product.

Inv

Imaginary inverse.

Loop

Loop.

Traits

Avatar

Implemented by avatars.

Commutative

Implememnted by commutative products.

Contravariant

Implemented by contravariant products.

LoopWitness

Loop Witness.

NonUniform

Implemented by avatars that have their “clothes off”.

Product

Implemented by products.

Uniform

Implemented by avatars that have their “clothes on”.

Functions

left_cover_by_proof

a ∧ b => -(a * b) = (-a) * b.

right_cover_by_proof

a ∧ b => -(a * b) = a * (-b).

to_loop

Gets a loop witness from product witness.