lean-bindings-0.1: Haskell bindings to the Lean Theorem Prover.

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

Language.Lean.Internal.Univ

Contents

Internal Operations

Description

Internal declarations for Lean universe values together with typeclass instances for Univ.

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

showUniv :: Univ -> String Source

Show a universe.

showUnivUsing :: Univ -> Options -> String Source

Show a universe with the given options.

univLt :: Univ -> Univ -> Bool Source

Total ordering over universes using structural equality.

Internal Operations

type UnivPtr = Ptr Univ Source

Haskell type for lean_univ FFI parameters.

type OutUnivPtr = Ptr UnivPtr Source

Haskell type for lean_univ* FFI parameters.

withUniv :: Univ -> (Ptr Univ -> IO a) -> IO a Source

Function c2hs uses to pass Univ values to Lean

type ListUniv = List Univ Source

Synonym for List Expr that can be used in c2hs bindings

type ListUnivPtr = Ptr ListUniv Source

Haskell type for lean_list_univ FFI parameters.

type OutListUnivPtr = Ptr ListUnivPtr Source

Haskell type for lean_list_univ* FFI parameters.

withListUniv :: ListUniv -> (Ptr ListUniv -> IO a) -> IO a Source

Function c2hs uses to pass ListUniv values to Lean