Copyright	(c) Galois Inc, 2015
License	Apache-2
Maintainer	jhendrix@galois.com, lcasburn@galois.com
Safe Haskell	Trustworthy
Language	Haskell98

Language.Lean.Univ

Contents

Operations on universe levels

Description

Operations for universe levels.

Synopsis

Documentation

data Univ Source

A Lean universe level

Instances

Eq Univ Source
Ord Univ Source
Show Univ Source
IsLeanValue Univ (Ptr Univ) Source
IsList (List Univ) Source	Allow `(List Univ)` to use `OverloadedLists` extensions.
Eq (List Univ) Source
Show (List Univ) Source
IsListIso (List Univ) Source
IsLeanValue (List Univ) (Ptr (List Univ)) Source
data List Univ = ListUniv (ForeignPtr (List Univ)) Source	A list of universes (constructor not actually exported)
type Item (List Univ) = Univ Source

zeroUniv :: Univ Source

The zero universe

succUniv :: Univ -> Univ Source

Successor of the universe

maxUniv :: Univ -> Univ -> Univ Source

The max of two universes.

imaxUniv :: Univ -> Univ -> Univ Source

The imax of two universes.

paramUniv :: Name -> Univ Source

A universe parameter of the given name.

globalUniv :: Name -> Univ Source

A global universe with the given name.

metaUniv :: Name -> Univ Source

A universe meta-variable with the given name.

explicitUniv :: Integer -> Univ Source

Create an explicit universe level

data UnivView Source

A view of a universe.

Constructors

UnivZero	The zero universe.
UnivSucc !Univ	Successor of the previous universe.
UnivMax !Univ !Univ	Maximum of two universes.
UnivIMax !Univ !Univ	`UnivIMax x y` denotes `y` if `y` is universe zero, otherwise `UnivMax x y`
UnivParam !Name	Universe parameter with the given name.
UnivGlobal !Name	Reference to a global universe.
UnivMeta !Name	Meta variable with the given name.

Instances

Eq UnivView Source
Ord UnivView Source
Show UnivView Source

univView :: Univ -> UnivView Source

Create a view of the universe.

showUniv :: Univ -> String Source

Show a universe.

showUnivUsing :: Univ -> Options -> String Source

Show a universe with the given options.

Operations on universe levels

normalizeUniv :: Univ -> Univ Source

Return the normal form for a universe.

instantiateUniv :: Univ -> [(Name, Univ)] -> Univ Source

Instantiate the parameters with universes

instantiateUniv2 :: Univ -> List Name -> List Univ -> Univ Source

Instantiate the parameters with universes using separate lists for names and levels.

univGeq :: Univ -> Univ -> Bool Source

geqUniv x y returns true if y is a larger universe level than x for all possible assignments to the variables in the x and y.

univLt :: Univ -> Univ -> Bool Source

Total ordering over universes using structural equality.