package mugen

You can search for identifiers within the package.

in-package search v0.2.0

mugen
- Mugen
  - Semantics
    
    Endo
    
    Make
    
    P
    
    Shift
    
    Param
    
    Shift
    
    S
    
    Free
    
    Make
    
    Infix
    
    P
    
    Shift
    
    Param
    
    Shift
    
    S
    
    Infix
  - Shift
    
    Constant
    
    Act
    
    Const
    
    FiniteSupport
    
    Base
    
    Fractal
    
    Base
    
    Int
    
    Lexicographic
    
    X
    
    Y
    
    Nat
    
    NearlyConstant
    
    Base
    
    NonPositive
    
    Opposite
    
    Base
    
    Prefix
    
    Base
    
    Product
    
    X
    
    Y
    
    S
  - ShiftWithJoin
    
    BoundedSemilattice
    
    FiniteSupport
    
    Base
    
    Int
    
    Lexicographic
    
    X
    
    Y
    
    Nat
    
    NearlyConstant
    
    Base
    
    NonPositive
    
    Product
    
    X
    
    Y
    
    Semilattice
  - StructuredType
    
    EqualityType
    
    PartiallyOrderedType
    
    PartiallyOrderedTypeWithRightAction
  - Syntax
    
    Endo
    
    Free

Legend:
Library
Module
Module type
Parameter
Class
Class type

To form a valid displacement algebra, compose and id should form a monoid, and lt (the strict order) must be left-invariant respect to compose.

include StructuredType.PartiallyOrderedType

include StructuredType.EqualityType

type t

The type.

val equal : t -> t -> bool

equal x y checks whether x and y are equivalent.

val dump : Format.formatter -> t -> unit

Ugly printer.

val lt : t -> t -> bool

lt x y checks if x is strictly less than y. Note that trichotomy fails for general partial orders.

val leq : t -> t -> bool

leq x y checks if x is less than or equal to y. Note that trichotomy fails for general partial orders.

val id : t

id is the unit.

val is_id : t -> bool

is_id s checks whether s is the unit. It is equivalent to equal id s, but potentially faster.

val compose : t -> t -> t

compose s1 s2 composes the operators s1 and s2. Note that Foo^s1^s2 in McBride's notation is understood as compose (compose ... s2) s1 with the reversed order.