Core.Binary.Prims

Reexports

Definitions

data Bin : Type

Totality: total
Visibility: export

data ResID : Type

Totality: total
Visibility: export

interface TTC : Type -> Type

Parameters: a
Methods:

toBuf : Ref Bin Binary => a -> Core ()

fromBuf : Ref Bin Binary => Core a

Implementations:

TTC Decoration

TTC Metadata

TTC TTMFile

TTC Int

TTC String

TTC Binary

TTC Bool

TTC Char

TTC Double

(TTC a, TTC b) => TTC (a, b)

TTC ()

(TTC a, TTC (p y)) => TTC (DPair a p)

TTC a => TTC (Maybe a)

TTC a => TTC (WithDefault a def)

(TTC a, TTC b) => TTC (Either a b)

TTC a => TTC (List a)

TTC a => TTC (List1 a)

TTC a => TTC (Vect n a)

(TTC a, Measure a) => TTC (PosMap a)

TTC Integer

TTC Bits8

TTC Bits16

TTC Bits32

TTC Bits64

TTC Int8

TTC Int16

TTC Int32

TTC Int64

TTC Nat

TTC NatSet

TTC a => TTC (SnocList a)

TTC InlineOk

TTC Namespace

TTC ModuleIdent

TTC VirtualIdent

TTC OriginDesc

TTC FC

TTC Name

TTC RigCount

TTC t => TTC (PiInfo t)

TTC t => TTC (PiBindData t)

All (TTC . type) fs => TTC (Record fs)

All (TTC . type) fs => TTC a => TTC (WithData fs a)

TTC PrimType

TTC Constant

TTC LazyReason

TTC NameType

TTC (Binder (Term vars))

TTC UseSide

TTC (Term vars)

TTC Pat

TTC (CaseTree vars)

TTC (CaseAlt vars)

TTC (Env Term vars)

TTC Visibility

TTC PartialReason

TTC Terminating

TTC Covering

TTC Totality

TTC (PrimFn n)

TTC ConInfo

TTC (CExp vars)

TTC (CConAlt vars)

TTC (CConstAlt vars)

TTC CFType

TTC CDef

TTC CG

TTC PairNames

TTC RewriteNames

TTC PrimNames

TTC HoleInfo

TTC PMDefInfo

TTC TypeFlags

TTC Def

TTC TotalReq

TTC DefFlag

TTC SizeChange

TTC SCCall

TTC GlobalDef

TTC Transform

toBuf : TTC a => Ref Bin Binary => a -> Core ()

Visibility: public export

fromBuf : TTC a => Ref Bin Binary => Core a

Visibility: public export

initBinary : Core (Ref Bin Binary)

Visibility: export

initBinaryS : Int -> Core (Ref Bin Binary)

Visibility: export

corrupt : String -> Core a

Visibility: export

tag : Ref Bin Binary => Int -> Core ()

Visibility: export

getTag : Ref Bin Binary => Core Int

Visibility: export

modTime : String -> Core Timestamp

  Get a file's modified time. If it doesn't exist, return 0 (UNIX Epoch)

Visibility: export

hashFileWith : Maybe String -> String -> Core (Maybe String)

Visibility: export