Module Mugen.Syntax

Definitions of level expressions

type ('s, 'a) endo =
  1. | Shifted of 'a * 's
  2. | Top

A family of polynomial endofunctors ('s, -) endo indexed by the type of displacements 's.

type ('s, 'v) free =
  1. | Level of ('s, ('s, 'v) free) endo
  2. | Var of 'v

The free monad ('s, -) free on the endofunctor ('s, -) endo indexed by the type of displacements 's.

module Endo : sig ... end

Stupid constructors for endo.

module Free : sig ... end

Stupid constructors for free.