package mugen

  1. Overview
  2. Docs

The implementation of smart constructors.

Parameters

module P : Param

Signature

type level = (P.Shift.t, P.var) Syntax.free

The type of freely generated levels.

val var : P.var -> level
val shifted : level -> P.Shift.t -> level

Smarter version of Syntax.Endo.shifted that collapses multiple displacements

val top : level
val equal : level -> level -> bool

equal l1 l2 checks whether l1 and l2 are the same universe level.

val lt : level -> level -> bool

lt l1 l2 checks whether l1 is strictly less than l2. Note that trichotomy fails for general universe levels.

val leq : level -> level -> bool

leq l1 l2 checks whether l1 is less than or equal to l2. Note that trichotomy fails for general universe levels.

val gt : level -> level -> bool

gt l1 l2 is lt l2 l1.

val geq : level -> level -> bool

geq l1 l2 is leq l2 l1.

module Infix : sig ... end

Infix notation.

OCaml

Innovation. Community. Security.