Math and math accessories. A place where I blow off some steam in the Lean proof assistant.
Tested with Lean Prover version 3.3.0.
sep
. Separation algebras. A separation algebra is a setS
together with an operator which mapsS*S
to the power-set ofS
. This operator is assumed to be commutative and (in an appropriate sense) associative. (See Bringing order to the separation logic jungle, by Cao, Cuellar, Appel.) We explore some of the algebraic properties of these structures.