Core.Primitives

Definitions

record Prim : Type

Totality: total
Visibility: public export
Constructor: 

MkPrim : PrimFn arity -> ClosedTerm -> Totality -> Prim

Projections:

.arity : Prim -> Nat

.fn : ({rec:0} : Prim) -> PrimFn (arity {rec:0})

.totality : Prim -> Totality

.type : Prim -> ClosedTerm

.arity : Prim -> Nat

Visibility: public export

arity : Prim -> Nat

Visibility: public export

.fn : ({rec:0} : Prim) -> PrimFn (arity {rec:0})

Visibility: public export

fn : ({rec:0} : Prim) -> PrimFn (arity {rec:0})

Visibility: public export

.type : Prim -> ClosedTerm

Visibility: public export

type : Prim -> ClosedTerm

Visibility: public export

.totality : Prim -> Totality

Visibility: public export

totality : Prim -> Totality

Visibility: public export

getOp : PrimFn arity -> Vect arity (NF vars) -> Maybe (NF vars)

Visibility: export

opName : PrimFn arity -> Name

Visibility: export

allPrimitives : List Prim

Visibility: export