Ordering

Imports
open Copy;
Table of Contents

Types

Ordering

(inductive)
inductive Ordering

Constructors

For each type in this module: inductive types list their declared constructors; opaque types list any local function whose name starts with mk and which returns a value of that type.

Ordering (inductive)

less

constructor
Ordering

equal

constructor
Ordering

greater

constructor
Ordering

Functions

compareInt

def compareInt (x : Int) (y : Int) : Ordering