IdrisDoc: [builtins]

[builtins]

(~=~) : (x : a) -> (y : b) -> Type

Explicit heterogeneous ("John Major") equality. Use this when Idris
incorrectly chooses homogeneous equality for (=).

Fixity
Non-associative, precedence 5
a

the type of the left side

b

the type of the right side

x

the left side

y

the right side

void : Void -> a

The eliminator for the Void type.

unsafePerformPrimIO : PrimIO a -> a
unsafePerformIO : IO' ffi a -> a
trans : (a = b) -> (b = c) -> a = c

Transitivity of propositional equality

sym : (l = r) -> r = l

Symmetry of propositional equality

run__provider : IO a -> PrimIO a
run__IO : IO' l () -> PrimIO ()
replace : (x = y) -> P x -> P y

Perform substitution in a term according to some equality.

This is used by the rewrite tactic and term.

really_believe_me : a -> b

Subvert the type checker. This function will reduce in the type checker.
Use it with extreme care - it can result in segfaults or worse!

prim_write : String -> IO' l Int
prim_read : IO' l String
prim_lenString : String -> Int
prim_io_return : a -> PrimIO a
prim_io_bind : PrimIO a -> (a -> PrimIO b) -> PrimIO b
prim_fwrite : Ptr -> String -> IO' l Int
prim_fread : Ptr -> IO' l String
prim_fork : PrimIO () -> PrimIO Ptr
prim__zextInt_BigInt : Int -> Integer
prim__zextInt_B64 : Int -> Bits64
prim__zextInt_B32 : Int -> Bits32
prim__zextInt_B16 : Int -> Bits16
prim__zextChar_BigInt : Char -> Integer
prim__zextB8_Int : Bits8 -> Int
prim__zextB8_BigInt : Bits8 -> Integer
prim__zextB8_B64 : Bits8 -> Bits64
prim__zextB8_B32 : Bits8 -> Bits32
prim__zextB8_B16 : Bits8 -> Bits16
prim__zextB64_BigInt : Bits64 -> Integer
prim__zextB32_Int : Bits32 -> Int
prim__zextB32_BigInt : Bits32 -> Integer
prim__zextB32_B64 : Bits32 -> Bits64
prim__zextB16_Int : Bits16 -> Int
prim__zextB16_BigInt : Bits16 -> Integer
prim__zextB16_B64 : Bits16 -> Bits64
prim__zextB16_B32 : Bits16 -> Bits32
prim__xorInt : Int -> Int -> Int
prim__xorChar : Char -> Char -> Char
prim__xorBigInt : Integer -> Integer -> Integer
prim__xorB8 : Bits8 -> Bits8 -> Bits8
prim__xorB64 : Bits64 -> Bits64 -> Bits64
prim__xorB32 : Bits32 -> Bits32 -> Bits32
prim__xorB16 : Bits16 -> Bits16 -> Bits16
prim__writeString : prim__WorldType -> String -> Int
prim__writeFile : prim__WorldType -> Ptr -> String -> Int
prim__vm : Ptr
prim__uremInt : Int -> Int -> Int
prim__uremChar : Char -> Char -> Char
prim__uremBigInt : Integer -> Integer -> Integer
prim__uremB8 : Bits8 -> Bits8 -> Bits8
prim__uremB64 : Bits64 -> Bits64 -> Bits64
prim__uremB32 : Bits32 -> Bits32 -> Bits32
prim__uremB16 : Bits16 -> Bits16 -> Bits16
prim__udivInt : Int -> Int -> Int
prim__udivChar : Char -> Char -> Char
prim__udivBigInt : Integer -> Integer -> Integer
prim__udivB8 : Bits8 -> Bits8 -> Bits8
prim__udivB64 : Bits64 -> Bits64 -> Bits64
prim__udivB32 : Bits32 -> Bits32 -> Bits32
prim__udivB16 : Bits16 -> Bits16 -> Bits16
prim__truncInt_B8 : Int -> Bits8
prim__truncInt_B64 : Int -> Bits64
prim__truncInt_B32 : Int -> Bits32
prim__truncInt_B16 : Int -> Bits16
prim__truncBigInt_Int : Integer -> Int
prim__truncBigInt_Char : Integer -> Char
prim__truncBigInt_B8 : Integer -> Bits8
prim__truncBigInt_B64 : Integer -> Bits64
prim__truncBigInt_B32 : Integer -> Bits32
prim__truncBigInt_B16 : Integer -> Bits16
prim__truncB64_Int : Bits64 -> Int
prim__truncB64_B8 : Bits64 -> Bits8
prim__truncB64_B32 : Bits64 -> Bits32
prim__truncB64_B16 : Bits64 -> Bits16
prim__truncB32_Int : Bits32 -> Int
prim__truncB32_B8 : Bits32 -> Bits8
prim__truncB32_B16 : Bits32 -> Bits16
prim__truncB16_Int : Bits16 -> Int
prim__truncB16_B8 : Bits16 -> Bits8
prim__toStrInt : Int -> String
prim__toStrChar : Char -> String
prim__toStrBigInt : Integer -> String
prim__toStrB8 : Bits8 -> String
prim__toStrB64 : Bits64 -> String
prim__toStrB32 : Bits32 -> String
prim__toStrB16 : Bits16 -> String
prim__toFloatInt : Int -> Double
prim__toFloatChar : Char -> Double
prim__toFloatBigInt : Integer -> Double
prim__toFloatB8 : Bits8 -> Double
prim__toFloatB64 : Bits64 -> Double
prim__toFloatB32 : Bits32 -> Double
prim__toFloatB16 : Bits16 -> Double
prim__systemInfo : Int -> String
prim__syntactic_eq : (a : Type) -> (b : Type) -> (x : a) -> (y : b) -> Maybe (x = y)
prim__subInt : Int -> Int -> Int
prim__subFloat : Double -> Double -> Double
prim__subChar : Char -> Char -> Char
prim__subBigInt : Integer -> Integer -> Integer
prim__subB8 : Bits8 -> Bits8 -> Bits8
prim__subB64 : Bits64 -> Bits64 -> Bits64
prim__subB32 : Bits32 -> Bits32 -> Bits32
prim__subB16 : Bits16 -> Bits16 -> Bits16
prim__strToFloat : String -> Double
prim__strTail : String -> String
prim__strRev : String -> String
prim__strIndex : String -> Int -> Char
prim__strHead : String -> Char
prim__strCons : Char -> String -> String
prim__stdout : Ptr
prim__stdin : Ptr
prim__stderr : Ptr
prim__sremInt : Int -> Int -> Int
prim__sremChar : Char -> Char -> Char
prim__sremBigInt : Integer -> Integer -> Integer
prim__sremB8 : Bits8 -> Bits8 -> Bits8
prim__sremB64 : Bits64 -> Bits64 -> Bits64
prim__sremB32 : Bits32 -> Bits32 -> Bits32
prim__sremB16 : Bits16 -> Bits16 -> Bits16
prim__slteInt : Int -> Int -> Int
prim__slteFloat : Double -> Double -> Int
prim__slteChar : Char -> Char -> Int
prim__slteBigInt : Integer -> Integer -> Int
prim__slteB8 : Bits8 -> Bits8 -> Int
prim__slteB64 : Bits64 -> Bits64 -> Int
prim__slteB32 : Bits32 -> Bits32 -> Int
prim__slteB16 : Bits16 -> Bits16 -> Int
prim__sltInt : Int -> Int -> Int
prim__sltFloat : Double -> Double -> Int
prim__sltChar : Char -> Char -> Int
prim__sltBigInt : Integer -> Integer -> Int
prim__sltB8 : Bits8 -> Bits8 -> Int
prim__sltB64 : Bits64 -> Bits64 -> Int
prim__sltB32 : Bits32 -> Bits32 -> Int
prim__sltB16 : Bits16 -> Bits16 -> Int
prim__shlInt : Int -> Int -> Int
prim__shlChar : Char -> Char -> Char
prim__shlBigInt : Integer -> Integer -> Integer
prim__shlB8 : Bits8 -> Bits8 -> Bits8
prim__shlB64 : Bits64 -> Bits64 -> Bits64
prim__shlB32 : Bits32 -> Bits32 -> Bits32
prim__shlB16 : Bits16 -> Bits16 -> Bits16
prim__sgteInt : Int -> Int -> Int
prim__sgteFloat : Double -> Double -> Int
prim__sgteChar : Char -> Char -> Int
prim__sgteBigInt : Integer -> Integer -> Int
prim__sgteB8 : Bits8 -> Bits8 -> Int
prim__sgteB64 : Bits64 -> Bits64 -> Int
prim__sgteB32 : Bits32 -> Bits32 -> Int
prim__sgteB16 : Bits16 -> Bits16 -> Int
prim__sgtInt : Int -> Int -> Int
prim__sgtFloat : Double -> Double -> Int
prim__sgtChar : Char -> Char -> Int
prim__sgtBigInt : Integer -> Integer -> Int
prim__sgtB8 : Bits8 -> Bits8 -> Int
prim__sgtB64 : Bits64 -> Bits64 -> Int
prim__sgtB32 : Bits32 -> Bits32 -> Int
prim__sgtB16 : Bits16 -> Bits16 -> Int
prim__sextInt_BigInt : Int -> Integer
prim__sextInt_B64 : Int -> Bits64
prim__sextInt_B32 : Int -> Bits32
prim__sextInt_B16 : Int -> Bits16
prim__sextChar_BigInt : Char -> Integer
prim__sextB8_Int : Bits8 -> Int
prim__sextB8_BigInt : Bits8 -> Integer
prim__sextB8_B64 : Bits8 -> Bits64
prim__sextB8_B32 : Bits8 -> Bits32
prim__sextB8_B16 : Bits8 -> Bits16
prim__sextB64_BigInt : Bits64 -> Integer
prim__sextB32_Int : Bits32 -> Int
prim__sextB32_BigInt : Bits32 -> Integer
prim__sextB32_B64 : Bits32 -> Bits64
prim__sextB16_Int : Bits16 -> Int
prim__sextB16_BigInt : Bits16 -> Integer
prim__sextB16_B64 : Bits16 -> Bits64
prim__sextB16_B32 : Bits16 -> Bits32
prim__sdivInt : Int -> Int -> Int
prim__sdivChar : Char -> Char -> Char
prim__sdivBigInt : Integer -> Integer -> Integer
prim__sdivB8 : Bits8 -> Bits8 -> Bits8
prim__sdivB64 : Bits64 -> Bits64 -> Bits64
prim__sdivB32 : Bits32 -> Bits32 -> Bits32
prim__sdivB16 : Bits16 -> Bits16 -> Bits16
prim__registerPtr : Ptr -> Int -> ManagedPtr
prim__readString : prim__WorldType -> String
prim__readFile : prim__WorldType -> Ptr -> String
prim__orInt : Int -> Int -> Int
prim__orChar : Char -> Char -> Char
prim__orBigInt : Integer -> Integer -> Integer
prim__orB8 : Bits8 -> Bits8 -> Bits8
prim__orB64 : Bits64 -> Bits64 -> Bits64
prim__orB32 : Bits32 -> Bits32 -> Bits32
prim__orB16 : Bits16 -> Bits16 -> Bits16
prim__null : Ptr
prim__negFloat : Double -> Double
prim__mulInt : Int -> Int -> Int
prim__mulFloat : Double -> Double -> Double
prim__mulChar : Char -> Char -> Char
prim__mulBigInt : Integer -> Integer -> Integer
prim__mulB8 : Bits8 -> Bits8 -> Bits8
prim__mulB64 : Bits64 -> Bits64 -> Bits64
prim__mulB32 : Bits32 -> Bits32 -> Bits32
prim__mulB16 : Bits16 -> Bits16 -> Bits16
prim__lteChar : Char -> Char -> Int
prim__lteBigInt : Integer -> Integer -> Int
prim__lteB8 : Bits8 -> Bits8 -> Int
prim__lteB64 : Bits64 -> Bits64 -> Int
prim__lteB32 : Bits32 -> Bits32 -> Int
prim__lteB16 : Bits16 -> Bits16 -> Int
prim__ltString : String -> String -> Int
prim__ltChar : Char -> Char -> Int
prim__ltBigInt : Integer -> Integer -> Int
prim__ltB8 : Bits8 -> Bits8 -> Int
prim__ltB64 : Bits64 -> Bits64 -> Int
prim__ltB32 : Bits32 -> Bits32 -> Int
prim__ltB16 : Bits16 -> Bits16 -> Int
prim__lshrInt : Int -> Int -> Int
prim__lshrChar : Char -> Char -> Char
prim__lshrBigInt : Integer -> Integer -> Integer
prim__lshrB8 : Bits8 -> Bits8 -> Bits8
prim__lshrB64 : Bits64 -> Bits64 -> Bits64
prim__lshrB32 : Bits32 -> Bits32 -> Bits32
prim__lshrB16 : Bits16 -> Bits16 -> Bits16
prim__intToChar : Int -> Char
prim__gteChar : Char -> Char -> Int
prim__gteBigInt : Integer -> Integer -> Int
prim__gteB8 : Bits8 -> Bits8 -> Int
prim__gteB64 : Bits64 -> Bits64 -> Int
prim__gteB32 : Bits32 -> Bits32 -> Int
prim__gteB16 : Bits16 -> Bits16 -> Int
prim__gtChar : Char -> Char -> Int
prim__gtBigInt : Integer -> Integer -> Int
prim__gtB8 : Bits8 -> Bits8 -> Int
prim__gtB64 : Bits64 -> Bits64 -> Int
prim__gtB32 : Bits32 -> Bits32 -> Int
prim__gtB16 : Bits16 -> Bits16 -> Int
prim__fromStrInt : String -> Int
prim__fromStrChar : String -> Char
prim__fromStrBigInt : String -> Integer
prim__fromStrB8 : String -> Bits8
prim__fromStrB64 : String -> Bits64
prim__fromStrB32 : String -> Bits32
prim__fromStrB16 : String -> Bits16
prim__fromFloatInt : Double -> Int
prim__fromFloatChar : Double -> Char
prim__fromFloatBigInt : Double -> Integer
prim__fromFloatB8 : Double -> Bits8
prim__fromFloatB64 : Double -> Bits64
prim__fromFloatB32 : Double -> Bits32
prim__fromFloatB16 : Double -> Bits16
prim__floatToStr : Double -> String
prim__floatTan : Double -> Double
prim__floatSqrt : Double -> Double
prim__floatSin : Double -> Double
prim__floatLog : Double -> Double
prim__floatFloor : Double -> Double
prim__floatExp : Double -> Double
prim__floatCos : Double -> Double
prim__floatCeil : Double -> Double
prim__floatATan : Double -> Double
prim__floatASin : Double -> Double
prim__floatACos : Double -> Double
prim__eqString : String -> String -> Int
prim__eqPtr : Ptr -> Ptr -> Int
prim__eqManagedPtr : ManagedPtr -> ManagedPtr -> Int
prim__eqInt : Int -> Int -> Int
prim__eqFloat : Double -> Double -> Int
prim__eqChar : Char -> Char -> Int
prim__eqBigInt : Integer -> Integer -> Int
prim__eqB8 : Bits8 -> Bits8 -> Int
prim__eqB64 : Bits64 -> Bits64 -> Int
prim__eqB32 : Bits32 -> Bits32 -> Int
prim__eqB16 : Bits16 -> Bits16 -> Int
prim__divFloat : Double -> Double -> Double
prim__concat : String -> String -> String
prim__complInt : Int -> Int
prim__complChar : Char -> Char
prim__complBigInt : Integer -> Integer
prim__complB8 : Bits8 -> Bits8
prim__complB64 : Bits64 -> Bits64
prim__complB32 : Bits32 -> Bits32
prim__complB16 : Bits16 -> Bits16
prim__charToInt : Char -> Int
prim__believe_me : (a : Type) -> (b : Type) -> (x : a) -> b
prim__ashrInt : Int -> Int -> Int
prim__ashrChar : Char -> Char -> Char
prim__ashrBigInt : Integer -> Integer -> Integer
prim__ashrB8 : Bits8 -> Bits8 -> Bits8
prim__ashrB64 : Bits64 -> Bits64 -> Bits64
prim__ashrB32 : Bits32 -> Bits32 -> Bits32
prim__ashrB16 : Bits16 -> Bits16 -> Bits16
prim__andInt : Int -> Int -> Int
prim__andChar : Char -> Char -> Char
prim__andBigInt : Integer -> Integer -> Integer
prim__andB8 : Bits8 -> Bits8 -> Bits8
prim__andB64 : Bits64 -> Bits64 -> Bits64
prim__andB32 : Bits32 -> Bits32 -> Bits32
prim__andB16 : Bits16 -> Bits16 -> Bits16
prim__addInt : Int -> Int -> Int
prim__addFloat : Double -> Double -> Double
prim__addChar : Char -> Char -> Char
prim__addBigInt : Integer -> Integer -> Integer
prim__addB8 : Bits8 -> Bits8 -> Bits8
prim__addB64 : Bits64 -> Bits64 -> Bits64
prim__addB32 : Bits32 -> Bits32 -> Bits32
prim__addB16 : Bits16 -> Bits16 -> Bits16
par : Lazy a -> a
mkForeignPrim : ForeignPrimType xs env t
liftPrimIO : (World -> PrimIO a) -> IO' l a
io_return : a -> IO' l a
io_bind : IO' l a -> (a -> IO' l b) -> IO' l b
foreign_prim : (f : FFI) -> (fname : ffi_fn f) -> FTy f xs ty -> FEnv f xs -> ty
foreign : (f : FFI) -> (fname : ffi_fn f) -> (ty : Type) -> {auto fty : FTy f [] ty} -> ty

Call a foreign function.

The particular semantics of foreign function calls depend on the
Idris compiler backend in use. For the default C backend, see the
documentation for FFI_C.

For more details, please consult the Idris documentation.

f

an FFI descriptor, which is specific to the compiler backend.

fname

the name of the foreign function

ty

the Idris type for the foreign function

fty

an automatically-found proof that the Idris type works with
the FFI in question

call__IO : IO' l a -> PrimIO a
believe_me : a -> b

Subvert the type checker. This function is abstract, so it will not reduce in
the type checker. Use it with care - it can result in segfaults or worse!

assert_total : a -> a

Assert to the totality checker that the given expression will always
terminate.

assert_smaller : (x : a) -> (y : b) -> b

Assert to the totality checker that y is always structurally smaller than
x (which is typically a pattern argument)

x

the larger value (typically a pattern argument)

y

the smaller value (typically an argument to a recursive call)

applyEnv : (env : FEnv ffi xs) -> ForeignPrimType xs env t -> World -> ffi_fn ffi -> ffi_types ffi t -> PrimIO t
WorldRes : Type -> Type
data World : Type

A token representing the world, for use in IO

TheWorld : prim__WorldType -> World
data Void : Type

The empty type, also known as the trivially false proposition.

Use void or absurd to prove anything if you have a variable of type Void in scope.

data Unit : Type

The canonical single-element type, also known as the trivially
true proposition.

MkUnit : ()

The trivial constructor for ().

data Symbol_ : String -> Type

For 'symbol syntax. 'foo becomes Symbol_ "foo"

Ptr : Type
data PrimIO : Type -> Type

Idris's primitive IO, for building abstractions on top of

prim__IO : a -> PrimIO a
PE_uninhabited_b8cf8479 : Fin 0 -> Void
PE_uninhabited_7d42eb4b : Fin 0 -> Void
PE_traverse_be2479e2 : (a -> Maybe b) -> Binder a -> Maybe (Binder b)
PE_show_f8ea7192 : (x : (Int, Int)) -> String
PE_show_e05ee051 : (x : Integer) -> String
PE_show_c3d1fb1e : (x : List String) -> String
PE_show_9dc475d3 : (x : TT) -> String
PE_show_780eefa3 : (x : Int) -> String
PE_show_75c4c529 : (x : List TTName) -> String
PE_show_6c064f96 : (x : TTName) -> String
PE_show_40e180c4 : (x : (TTName, TT)) -> String
PE_show_1ecdd21e : (x : List (TTName, TT)) -> String
PE_show_1423db60 : (x : List FunArg) -> String
PE_showPrec_fc85e7fb : (d : Prec) -> (x : SpecialName) -> String
PE_showPrec_f6623b2f : (d : Prec) -> (x : Integer) -> String
PE_showPrec_f648ada3 : (d : Prec) -> (x : IntTy) -> String
PE_showPrec_e25a0007 : (d : Prec) -> (x : Bits16) -> String
PE_showPrec_dcccd8f9 : (d : Prec) -> (x : Binder TT) -> String
PE_showPrec_da29594a : (d : Prec) -> (x : Binder Raw) -> String
PE_showPrec_d04a7607 : (d : Prec) -> (x : Bits32) -> String
PE_showPrec_c4384170 : (d : Prec) -> (x : NameType) -> String
PE_showPrec_b7654048 : (d : Prec) -> (x : List String) -> String
PE_showPrec_a53cdf41 : (d : Prec) -> (x : List FunArg) -> String
PE_showPrec_9856cdaa : (d : Prec) -> (x : Int) -> String
PE_showPrec_8facfe9a : (d : Prec) -> (x : TTUExp) -> String
PE_showPrec_83e7f496 : (d : Prec) -> (x : Erasure) -> String
PE_showPrec_8375ad00 : (d : Prec) -> (x : Bool) -> String
PE_showPrec_7cb60871 : (d : Prec) -> (x : ArithTy) -> String
PE_showPrec_7a8cc9bf : (d : Prec) -> (x : Bits64) -> String
PE_showPrec_7900b24c : (d : Prec) -> (x : (Int, Int)) -> String
PE_showPrec_7600cc65 : (d : Prec) -> (x : List (TTName, TT)) -> String
PE_showPrec_67a4cb3f : (d : Prec) -> (x : String) -> String
PE_showPrec_4ee8ecec : (d : Prec) -> (x : List TTName) -> String
PE_showPrec_48ef1940 : (d : Prec) -> (x : FunArg) -> String
PE_showPrec_2d689550 : (d : Prec) -> (x : Bits8) -> String
PE_showPrec_2430a67 : (d : Prec) -> (x : Char) -> String
PE_showPrec_1be89e3c : (d : Prec) -> (x : Plicity) -> String
PE_showPrec_1b9c7d44 : (d : Prec) -> (x : Const) -> String
PE_showPrec_1856f7d5 : (d : Prec) -> (x : Double) -> String
PE_showPrec_10788e79 : (d : Prec) -> (x : NativeTy) -> String
PE_showArg_fe8a8f77 : (x : Plicity) -> String
PE_showArg_e456eb61 : (x : Bits8) -> String
PE_showArg_e05ee051 : (x : Integer) -> String
PE_showArg_e0274278 : (x : Bool) -> String
PE_showArg_dd3bae33 : (x : Bits32) -> String
PE_showArg_cebaaccd : (x : Bits64) -> String
PE_showArg_c9cb0e2 : (x : NativeTy) -> String
PE_showArg_c0cf4f29 : (x : Bits16) -> String
PE_showArg_b516e1f1 : (x : Raw) -> String
PE_showArg_b0644e35 : (x : SpecialName) -> String
PE_showArg_af3dc073 : (x : List String) -> String
PE_showArg_a8f161da : (x : ArithTy) -> String
PE_showArg_9dc475d3 : (x : TT) -> String
PE_showArg_9be0315 : (x : List (TTName, TT)) -> String
PE_showArg_919c1cf7 : (x : List FunArg) -> String
PE_showArg_91257ed0 : (x : Const) -> String
PE_showArg_8a83d648 : (x : Erasure) -> String
PE_showArg_8898e97e : (x : FunArg) -> String
PE_showArg_79ed54b4 : (x : Binder Raw) -> String
PE_showArg_780eefa3 : (x : Int) -> String
PE_showArg_6e15fe35 : (x : List TTName) -> String
PE_showArg_6c064f96 : (x : TTName) -> String
PE_showArg_6175fd1e : (x : Binder TT) -> String
PE_showArg_5bb34357 : (x : TTUExp) -> String
PE_showArg_4f8b5db8 : (x : (Int, Int)) -> String
PE_showArg_402fc88a : (x : Char) -> String
PE_showArg_3d04013f : (x : IntTy) -> String
PE_showArg_3cb0c48d : (x : NameType) -> String
PE_showArg_39883a05 : (x : Double) -> String
PE_showArg_237f4115 : (x : Err) -> String
PE_showArg_21ca3a08 : (x : String) -> String
PE_return_35b6d2aa : a -> IO' ffi a
PE_return_225b07b7 : a -> List a
PE_quotedTy_d790f77d : TT
PE_quotedTy_cc46ce21 : TT
PE_quotedTy_957b72f1 : Raw
PE_quotedTy_82972049 : Raw
PE_quote_f25f38ec : NativeTy -> TT
PE_quote_f171225 : Bits8 -> TT
PE_quote_ec0e14bd : Double -> Raw
PE_quote_e8e601cf : Raw -> TT
PE_quote_e7239409 : Bits16 -> TT
PE_quote_e63fa915 : TTName -> Raw
PE_quote_d7c6311a : List String -> TT
PE_quote_d6616d9d : Char -> Raw
PE_quote_d2171aa6 : Bits32 -> Raw
PE_quote_d0602b89 : Universe -> Raw
PE_quote_cf3a428a : Bits64 -> TT
PE_quote_c9afe6d8 : String -> TT
PE_quote_c25a0d9 : ArithTy -> Raw
PE_quote_abbde5ca : Integer -> TT
PE_quote_a5e1ede7 : Bits32 -> TT
PE_quote_a4bc2bf5 : List String -> Raw
PE_quote_a4744936 : Nat -> TT
PE_quote_9dbef66f : Double -> TT
PE_quote_9da2d1ab : Const -> TT
PE_quote_9617bbfd : TTUExp -> TT
PE_quote_9077a10b : NativeTy -> Raw
PE_quote_8aaf79d7 : Bits16 -> Raw
PE_quote_6c0c0f57 : IntTy -> Raw
PE_quote_66e4cf3f : NameType -> TT
PE_quote_54f0ae89 : Universe -> TT
PE_quote_54eb7f02 : ArithTy -> TT
PE_quote_534efb56 : Bits8 -> Raw
PE_quote_48365a58 : TTName -> TT
PE_quote_3deb0379 : Int -> Raw
PE_quote_2a84d628 : String -> Raw
PE_quote_27ac4bc8 : Integer -> Raw
PE_quote_264ccf36 : IntTy -> TT
PE_quote_233711a2 : Char -> TT
PE_quote_1ac4d11d : Const -> Raw
PE_quote_15dda697 : TT -> TT
PE_quote_1490a1d2 : Int -> TT
PE_quote_12a56711 : Bits64 -> Raw
PE_quote_1163ee77 : List ErrorReportPart -> TT
PE_pure_76b98f4 : a -> Maybe a
PE_pack_1b7ecec9 : List Char -> String
PE_neutral_42111bf0 : List b
PE_neutral_29ee08fd : List a
PE_negate_c4f9d4ec : Double -> Double
PE_negate_496236c : Double -> Double
PE_negate_47f40a8e : Integer -> Integer
PE_negate_35a146b7 : Int -> Int
PE_map_fa2fd5b0 : (m : a -> b) -> Vect k a -> Vect k b
PE_map_f7e727bb : (m : a -> b) -> Stream a -> Stream b
PE_map_a72e6f10 : (m : a -> b) -> List a -> List b
PE_map_9a5d1414 : (m : a -> b) -> Maybe a -> Maybe b
PE_isSuffixOf_4bcc612a : List Char -> List Char -> Bool
PE_isPrefixOf_4bcc612a : List Char -> List Char -> Bool
PE_isInfixOf_4bcc612a : List Char -> List Char -> Bool
PE_guard_c816fe1f : Bool -> List ()
PE_fromInteger_f88b56b2 : Integer -> Bits8
PE_fromInteger_ed894b53 : Integer -> Nat
PE_fromInteger_ec5da316 : Integer -> Bits16
PE_fromInteger_e347aa5d : Integer -> Bits32
PE_fromInteger_c4fa19c2 : Integer -> Double
PE_fromInteger_6d14b6dc : Integer -> Mod2 n
PE_fromInteger_47f3c5b8 : Integer -> Integer
PE_fromInteger_460ec151 : Integer -> Bits64
PE_fromInteger_35a18b8d : Integer -> Int
PE_foldr_fef28260 : (elt -> acc -> acc) -> acc -> List elt -> acc
PE_foldl_fef28260 : (acc -> elt -> acc) -> acc -> List elt -> acc
PE_empty_8ff8f7b3 : List a
PE_elem_4bcc612a : Char -> List Char -> Bool
PE_decEq_f66280a4 : (x1 : Nat) -> (x2 : Nat) -> Dec (x1 = x2)
PE_decEq_ac59f390 : (x1 : Bool) -> (x2 : Bool) -> Dec (x1 = x2)
PE_concat_159e5acd : List (List a) -> List a
PE_concatMap_fdbcf7d2 : (a -> List b) -> List a -> List b
PE_compare_e9e34a9b : Int -> Int -> Ordering
PE_compare_b9a3d0b5 : Integer -> Integer -> Ordering
PE_compare_9ec30338 : Nat -> Nat -> Ordering
PE_cast_e686c3c4 : (orig : Mod2 n) -> Bits n
PE_cast_e60b6fac : (orig : Int) -> Nat
PE_cast_c7549ffe : (orig : Fin n) -> Integer
PE_cast_bfb236e5 : (orig : Nat) -> Integer
PE_cast_a8bdef19 : (orig : Char) -> Int
PE_cast_961d3f22 : (orig : Nat) -> Int
PE_cast_92899844 : (orig : Int) -> Integer
PE_cast_8308e07c : (orig : String) -> List Char
PE_cast_5c6b350c : (orig : Int) -> Char
PE_cast_4e2b43a0 : (orig : Integer) -> Nat
PE_any_70e30afd : (a -> Bool) -> List a -> Bool
PE_absurd_680da6ae : (h : Fin 0) -> a
PE_abs_47f3c5b8 : Integer -> Integer
PE_abs_35a18b8d : Int -> Int
PE_Prelude.Show.List a instance of Prelude.Show.Show, method show_ecb8dd87 : (x : List (TTName, TT)) -> String
PE_Prelude.Show.List a instance of Prelude.Show.Show, method show_92ad42f9 : (x : List String) -> String
PE_Prelude.Show.List a instance of Prelude.Show.Show, method show_60210141 : (x : List TTName) -> String
PE_Prelude.Show.List a instance of Prelude.Show.Show, method show_50c8d5e1 : (x : List String) -> String
PE_Prelude.Show.List a instance of Prelude.Show.Show, method show_431960ce : (x : List (TTName, TT)) -> String
PE_Prelude.Show.List a instance of Prelude.Show.Show, method show_25230d09 : (x : List TTName) -> String
PE_Prelude.Show.List a instance of Prelude.Show.Show, method show_1ad2d1e1 : (x : List FunArg) -> String
PE_Prelude.Show.List a instance of Prelude.Show.Show, method show_10addef0 : (x : List FunArg) -> String
PE_Prelude.Show.List a instance of Prelude.Show.Show, method showPrec_9bbed635 : (d : Prec) -> (x : List TTName) -> String
PE_Prelude.Show.List a instance of Prelude.Show.Show, method showPrec_961c6e5c : (d : Prec) -> (x : List String) -> String
PE_Prelude.Show.List a instance of Prelude.Show.Show, method showPrec_8ad2f25e : (d : Prec) -> (x : List FunArg) -> String
PE_Prelude.Show.List a instance of Prelude.Show.Show, method showPrec_7c2b711f : (d : Prec) -> (x : List (TTName, TT)) -> String
PE_Prelude.Show.List a instance of Prelude.Show.Show, method showPrec_59ba85cd : (d : Prec) -> (x : List (TTName, TT)) -> String
PE_Prelude.Show.List a instance of Prelude.Show.Show, method showPrec_367b523c : (d : Prec) -> (x : List TTName) -> String
PE_Prelude.Show.List a instance of Prelude.Show.Show, method showPrec_2669bd4e : (d : Prec) -> (x : List FunArg) -> String
PE_Prelude.Show.List a instance of Prelude.Show.Show, method showPrec_17aa5d7f : (d : Prec) -> (x : List String) -> String
PE_Prelude.Show.(a, b) instance of Prelude.Show.Show, method show_cfed4029 : (x : (Int, Int)) -> String
PE_Prelude.Show.(a, b) instance of Prelude.Show.Show, method show_730b74b3 : (x : (TTName, TT)) -> String
PE_Prelude.Show.(a, b) instance of Prelude.Show.Show, method show_6c0a98ff : (x : (TTName, TT)) -> String
PE_Prelude.Show.(a, b) instance of Prelude.Show.Show, method show_34116f23 : (x : (Int, Int)) -> String
PE_Prelude.Show.(a, b) instance of Prelude.Show.Show, method showPrec_ed5db886 : (d : Prec) -> (x : (TTName, TT)) -> String
PE_Prelude.Show.(a, b) instance of Prelude.Show.Show, method showPrec_49c0ac27 : (d : Prec) -> (x : (Int, Int)) -> String
PE_Prelude.Show.(a, b) instance of Prelude.Show.Show, method showPrec_326abb01 : (d : Prec) -> (x : (Int, Int)) -> String
PE_Prelude.Show.(a, b) instance of Prelude.Show.Show, method showPrec_2b85f549 : (d : Prec) -> (x : (TTName, TT)) -> String
PE_Prelude.List.List a instance of Prelude.Classes.Eq, method /=_d76f9006 : List String -> List String -> Bool
PE_List a, TT instance of Language.Reflection.Quotable_c7b7686 : Quotable (List String) TT
PE_List a, TT instance of Language.Reflection.Quotable_61e53b8c : Quotable (List ErrorReportPart) TT
PE_List a, Raw instance of Language.Reflection.Quotable_1f79f810 : Quotable (List String) Raw
PE_List a instance of Prelude.Show.Show_f81aba2d : Show (List (TTName, TT))
PE_List a instance of Prelude.Show.Show_f4f80d17 : Show (List TTName)
PE_List a instance of Prelude.Show.Show_f0c6ce27 : Show (List (TTName, TT))
PE_List a instance of Prelude.Show.Show_e9c04f58 : Show (List String)
PE_List a instance of Prelude.Show.Show_e402a70f : Show (List TTName)
PE_List a instance of Prelude.Show.Show_9b02f8e9 : Show (List String)
PE_List a instance of Prelude.Show.Show_97031fb3 : Show (List FunArg)
PE_List a instance of Prelude.Show.Show_20fa57b2 : Show (List FunArg)
PE_List a instance of Prelude.Classes.Eq_8232b64 : Eq (List String)
PE_List a instance of Prelude.Classes.Eq_1ac0df3b : Eq (List String)
PE_Language.Reflection.Utils.Binder a instance of Prelude.Show.Show, method showPrec_e7742833 : (d : Prec) -> (x : Binder TT) -> String
PE_Language.Reflection.Utils.Binder a instance of Prelude.Show.Show, method showPrec_62d2c282 : (d : Prec) -> (x : Binder Raw) -> String
PE_Language.Reflection.List a, TT instance of Language.Reflection.Quotable, method quotedTy_12390fb7 : TT
PE_Language.Reflection.List a, TT instance of Language.Reflection.Quotable, method quote_b793517f : List ErrorReportPart -> TT
PE_Language.Reflection.List a, TT instance of Language.Reflection.Quotable, method quote_accf63b1 : List String -> TT
PE_Language.Reflection.List a, TT instance of Language.Reflection.Quotable, method quote_a6a4f90b : List String -> TT
PE_Language.Reflection.List a, Raw instance of Language.Reflection.Quotable, method quotedTy_b28d3d43 : Raw
PE_Language.Reflection.List a, Raw instance of Language.Reflection.Quotable, method quote_fbcb1ab4 : List String -> Raw
PE_Language.Reflection.List a, Raw instance of Language.Reflection.Quotable, method quote_2a0a7444 : List String -> Raw
PE_Language.Reflection.Binder instance of Prelude.Traversable.Traversable, method traverse_7170ca2e : (a -> Maybe b) -> Binder a -> Maybe (Binder b)
PE_Binder a instance of Prelude.Show.Show_7217f752 : Show (Binder Raw)
PE_Binder a instance of Prelude.Show.Show_67d34242 : Show (Binder TT)
PE_Binder a instance of Prelude.Classes.Eq_b1c68b68 : Eq (Binder TT)
PE_@@constructor of Prelude.Monad.Monad#Applicative m_d05ad59e : Applicative List
PE_@@constructor of Prelude.Applicative.Alternative#Applicative f_5102bba8 : Applicative List
PE_@@constructor of Prelude.Algebra.Monoid#Semigroup a_42111bf0 : Semigroup (List b)
PE_@@constructor of Prelude.Algebra.Monoid#Semigroup a_29ee08fd : Semigroup (List a)
PE_>_e9e34a9b : Int -> Int -> Bool
PE_>_b9a3d0b5 : Integer -> Integer -> Bool
PE_>_3b5d109d : Char -> Char -> Bool
PE_>>=_bf15fa2c : List a -> (a -> List b) -> List b
PE_>>=_113654bf : IO' ffi a -> (a -> IO' ffi b) -> IO' ffi b
PE_>=_e9e34a9b : Int -> Int -> Bool
PE_>=_b9a3d0b5 : Integer -> Integer -> Bool
PE_>=_55b2a078 : Prec -> Prec -> Bool
PE_>=_3b5d109d : Char -> Char -> Bool
PE_==_f89058ed : Bits8 -> Bits8 -> Bool
PE_==_ed844918 : Nat -> Nat -> Bool
PE_==_ec58a0db : Bits16 -> Bits16 -> Bool
PE_==_e34cac98 : Bits32 -> Bits32 -> Bool
PE_==_c4f51787 : Double -> Double -> Bool
PE_==_c1c7ee93 : Binder TT -> Binder TT -> Bool
PE_==_b9dcd481 : List String -> List String -> Bool
PE_==_b72e08d9 : NameType -> NameType -> Bool
PE_==_ac58518d : Fin n -> Fin n -> Bool
PE_==_a8175cce : Prec -> Prec -> Bool
PE_==_a2f52f49 : ManagedPtr -> ManagedPtr -> Bool
PE_==_a071205c : List String -> List String -> Bool
PE_==_99727393 : Ptr -> Ptr -> Bool
PE_==_905f6317 : Bool -> Bool -> Bool
PE_==_8df36628 : ArithTy -> ArithTy -> Bool
PE_==_8d5e505d : Const -> Const -> Bool
PE_==_76516bd2 : NativeTy -> NativeTy -> Bool
PE_==_6dbcd19f : Ordering -> Ordering -> Bool
PE_==_69fab30a : TTName -> TTName -> Bool
PE_==_62647925 : String -> String -> Bool
PE_==_5518d81a : IntTy -> IntTy -> Bool
PE_==_5497a012 : () -> () -> Bool
PE_==_4bcc612a : Char -> Char -> Bool
PE_==_47f8c7f3 : Integer -> Integer -> Bool
PE_==_4613c38c : Bits64 -> Bits64 -> Bool
PE_==_359c8952 : Int -> Int -> Bool
PE_==_326f514b : TTUExp -> TTUExp -> Bool
PE_<_e9e34a9b : Int -> Int -> Bool
PE_<_b9a3d0b5 : Integer -> Integer -> Bool
PE_<_644d9f86 : Double -> Double -> Bool
PE_<_11c58279 : Mod2 n -> Mod2 n -> Bool
PE_<=_e9e34a9b : Int -> Int -> Bool
PE_<=_b9a3d0b5 : Integer -> Integer -> Bool
PE_<=_3b5d109d : Char -> Char -> Bool
PE_<*>_4b446781 : Maybe (a -> b) -> Maybe a -> Maybe b
PE_/=_4bcc612a : Char -> Char -> Bool
PE_/=_359c8952 : Int -> Int -> Bool
PE_/=_3170a20a : Bits n -> Bits n -> Bool
PE_-_e9d2fd86 : Int -> Int -> Int
PE_-_b99383a0 : Integer -> Integer -> Integer
PE_-_9eb2b623 : Nat -> Nat -> Nat
PE_-_643d5271 : Double -> Double -> Double
PE_+_e9d2fd86 : Int -> Int -> Int
PE_+_b99383a0 : Integer -> Integer -> Integer
PE_+_9eb2b623 : Nat -> Nat -> Nat
PE_+_643d5271 : Double -> Double -> Double
PE_*_e9d2fd86 : Int -> Int -> Int
PE_*_b99383a0 : Integer -> Integer -> Integer
PE_*_9eb2b623 : Nat -> Nat -> Nat
PE_*_976370dc : Double -> Double -> Double
PE_*_643d5271 : Double -> Double -> Double
PE_(a, b) instance of Prelude.Show.Show_e603f950 : Show (Int, Int)
PE_(a, b) instance of Prelude.Show.Show_840828a3 : Show (Int, Int)
PE_(a, b) instance of Prelude.Show.Show_25774c0d : Show (TTName, TT)
PE_(a, b) instance of Prelude.Show.Show_214ea7bb : Show (TTName, TT)
ManagedPtr : Type
data LazyType : Type

There are two types of laziness: that arising from lazy functions, and that
arising from codata. They differ in their totality condition.

LazyCodata : LazyType
LazyEval : LazyType
data Lazy' : LazyType -> Type -> Type

The underlying implementation of Lazy and Inf.

Delay : (val : a) -> Lazy' t a

A delayed computation.

Delay is inserted automatically by the elaborator where necessary.

Note that compiled code gives Delay special semantics.

t

whether this is laziness from codata or normal lazy evaluation

a

the type of the eventual value

val

a computation that will produce a value

Lazy : Type -> Type

Lazily evaluated values. This has special evaluation semantics.

data JsFn : Type -> Type
MkJsFn : (x : t) -> JsFn t
data JS_Types : Type -> Type
JS_Str : JS_Types String
JS_Float : JS_Types Double
JS_Ptr : JS_Types Ptr
JS_Unit : JS_Types ()
JS_FnT : JS_FnTypes a -> JS_Types (JsFn a)
JS_IntT : JS_IntTypes i -> JS_Types i
data JS_IntTypes : Type -> Type
JS_IntChar : JS_IntTypes Char
JS_IntNative : JS_IntTypes Int
JS_IO : Type -> Type
data JS_FnTypes : Type -> Type
JS_Fn : JS_Types s -> JS_FnTypes t -> JS_FnTypes (s -> t)
JS_FnIO : JS_Types t -> JS_FnTypes (IO' l t)
JS_FnBase : JS_Types t -> JS_FnTypes t
Inf : Type -> Type

Recursive parameters to codata. Inserted automatically by the elaborator
on a "codata" definition but is necessary by hand if mixing inductive and
coinductive parameters.

data IO' : (lang : FFI) -> Type -> Type

The IO type, parameterised over the FFI that is available within
it.

MkIO : (World -> PrimIO a) -> IO' lang a
IO : Type -> Type
ForeignPrimType : (xs : List Type) -> FEnv ffi xs -> Type -> Type
Force : Lazy' t a -> a

Compute a value from a delayed computation.

Inserted by the elaborator where necessary.

Float : Type
data FTy : FFI -> List Type -> Type -> Type
FRet : ffi_types f t -> FTy f xs (IO' f t)
FFun : ffi_types f s -> FTy f (s :: xs) t -> FTy f xs (s -> t)
FFI_JS : FFI

The JavaScript FFI. The strings naming functions in this API are
JavaScript code snippets, into which the arguments are substituted
for the placeholders %0, %1, etc.

data FFI : Type

An FFI specifier, which describes how a particular compiler
backend handles foreign function calls.

MkFFI : (ffi_types : Type -> Type) -> (ffi_fn : Type) -> (ffi_data : Type) -> FFI
ffi_types

A family describing which types are available in the FFI

ffi_fn

The type used to specify the names of foreign functions in this FFI

ffi_data

How this FFI describes exported datatypes

data (=) : (x : A) -> (y : B) -> Type

The propositional equality type. A proof that x = y.

To use such a proof, pattern-match on it, and the two equal things will then need to be the same pattern.

Note: Idris's equality type is potentially heterogeneous, which means that it is possible to state equalities between values of potentially different types. However, Idris will attempt the homogeneous case unless it fails to typecheck.

You may need to use (~=~) to explicitly request heterogeneous equality.

A

the type of the left side of the equality

B

the type of the right side of the equality

Refl : x = x

A proof that x in fact equals x. To construct this, you must have already shown that both sides are in fact equal.

A

the type at which the equality is proven

x

the element shown to be equal to itself.