Mugen
module Shift : module type of Shift
Stock displacement algebras
module ShiftWithJoin : module type of ShiftWithJoin
Stock displacement algebras with joins
module Syntax : module type of Syntax
Definitions of level expressions
module Builder : module type of Builder
Smart constructors for level expressions
module Theory : module type of Theory
Semantic comparators for free level expressions