Idris2Doc : Core.TT.Primitive

Core.TT.Primitive

(source)
Definitions
data PrimType : Type
  Totality: total
  Visibility: public export
  Constructors:
  
IntType : PrimType
  
Int8Type : PrimType
  
Int16Type : PrimType
  
Int32Type : PrimType
  
Int64Type : PrimType
  
IntegerType : PrimType
  
Bits8Type : PrimType
  
Bits16Type : PrimType
  
Bits32Type : PrimType
  
Bits64Type : PrimType
  
StringType : PrimType
  
CharType : PrimType
  
DoubleType : PrimType
  
WorldType : PrimType

  Hints:
  
Eq PrimType
  
Hashable PrimType
  
Ord PrimType
  
Pretty IdrisSyntax PrimType
  
Reflect PrimType
  
Reify PrimType
  
Show PrimType
  
TTC 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
  
BI : Integer -> 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

  Hints:
  
Eq Constant
  
Hashable Constant
  
Ord Constant
  
Pretty IdrisSyntax Constant
  
Reflect Constant
  
Reify Constant
  
Show Constant
  
TTC Constant
primType : Constant -> Maybe PrimType
  Totality: total
  Visibility: export
isConstantType : Name -> Maybe PrimType
  Totality: total
  Visibility: export
isPrimType : Constant -> Bool
  Totality: total
  Visibility: export
primTypeEq : (x : PrimType) -> (y : PrimType) -> Maybe (x = y)
  Totality: total
  Visibility: export
constantEq : (x : Constant) -> (y : Constant) -> Maybe (x = y)
  Totality: total
  Visibility: export
primTypeTag : PrimType -> Int
  Totality: total
  Visibility: export
data Precision : Type
  Precision of integral types.

  Totality: total
  Visibility: public export
  Constructors:
  
P : Int -> Precision
  
Unlimited : Precision

  Hints:
  
Eq Precision
  
Ord Precision
data IntKind : Type
  Totality: total
  Visibility: public export
  Constructors:
  
Signed : Precision -> IntKind
  
Unsigned : Int -> IntKind
intKind : PrimType -> Maybe IntKind
  Totality: total
  Visibility: public export
precision : IntKind -> Precision
  Totality: total
  Visibility: public export
data PrimFn : Nat -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
Add : PrimType -> PrimFn 2
  
Sub : PrimType -> PrimFn 2
  
Mul : PrimType -> PrimFn 2
  
Div : PrimType -> PrimFn 2
  
Mod : PrimType -> PrimFn 2
  
Neg : PrimType -> PrimFn 1
  
ShiftL : PrimType -> PrimFn 2
  
ShiftR : PrimType -> PrimFn 2
  
BAnd : PrimType -> PrimFn 2
  
BOr : PrimType -> PrimFn 2
  
BXOr : PrimType -> PrimFn 2
  
LT : PrimType -> PrimFn 2
  
LTE : PrimType -> PrimFn 2
  
EQ : PrimType -> PrimFn 2
  
GTE : PrimType -> PrimFn 2
  
GT : PrimType -> PrimFn 2
  
StrLength : PrimFn 1
  
StrHead : PrimFn 1
  
StrTail : PrimFn 1
  
StrIndex : PrimFn 2
  
StrCons : PrimFn 2
  
StrAppend : PrimFn 2
  
StrReverse : PrimFn 1
  
StrSubstr : PrimFn 3
  
DoubleExp : PrimFn 1
  
DoubleLog : PrimFn 1
  
DoublePow : PrimFn 2
  
DoubleSin : PrimFn 1
  
DoubleCos : PrimFn 1
  
DoubleTan : PrimFn 1
  
DoubleASin : PrimFn 1
  
DoubleACos : PrimFn 1
  
DoubleATan : PrimFn 1
  
DoubleSqrt : PrimFn 1
  
DoubleFloor : PrimFn 1
  
DoubleCeiling : PrimFn 1
  
Cast : PrimType -> PrimType -> PrimFn 1
  
BelieveMe : PrimFn 3
  
Crash : PrimFn 2

  Hints:
  
Hashable (PrimFn arity)
  
Show (PrimFn arity)
  
TTC (PrimFn n)
prettyOp : PrimFn arity -> Vect arity (Doc IdrisSyntax) -> Doc IdrisSyntax
  Totality: total
  Visibility: export
primFnEq : PrimFn a1 -> PrimFn a2 -> Maybe (a1 = a2)
  Totality: total
  Visibility: export
primFnCmp : PrimFn a1 -> PrimFn a2 -> Ordering
  Totality: total
  Visibility: export