Serene.TT.Term

Definitions

Level : Type

Visibility: public export

data PrimType : Type

Totality: total
Visibility: public export
Constructors:

IntType : PrimType

Int8Type : PrimType

Int16Type : PrimType

Int32Type : PrimType

Int64Type : PrimType

Bits8Type : PrimType

Bits16Type : PrimType

Bits32Type : PrimType

Bits64Type : PrimType

StringType : PrimType

CharType : PrimType

DoubleType : PrimType

WorldType : PrimType

Hint: 

Show PrimType

data Constant : Type

Totality: total
Visibility: public export
Constructors:

I : Int -> Constant

I8 : Int8 -> Constant

I16 : Int16 -> Constant

I32 : Int32 -> Constant

I64 : Int64 -> Constant

B8 : Bits8 -> Constant

B16 : Bits16 -> Constant

B32 : Bits32 -> Constant

B64 : Bits64 -> Constant

Str : String -> Constant

Ch : Char -> Constant

Db : Double -> Constant

PrT : PrimType -> Constant

WorldVal : Constant

Hint: 

Show Constant

data Term : Type

  Core TT Term type.

Totality: total
Visibility: public export
Constructors:

Const : Metadata -> Constant -> Term

Var : Metadata -> Name -> Term

Lam : Metadata -> Name -> Term -> Term -> Term

Pi : Metadata -> Name -> Term -> Term -> Term

App : Metadata -> Term -> Term -> Term

Ann : Metadata -> Term -> Term -> Term

Let : Metadata -> Name -> Term -> Term -> Term -> Term

U : Metadata -> Level -> Term

MetaVar : Metadata -> Name -> Term

Hints:

HasMetadata Term

Show Term