Idris2Doc : Prelude.Cast

Prelude.Cast

Definitions

interfaceCast : Type->Type->Type
  Interface for transforming an instance of a data type to another type.

Parameters: from, to
Constructor: 
MkCast

Methods:
cast : from->to
  Perform a (potentially lossy!) cast operation.
@ orig The original type

Implementations:
Castaa
CastIntString
CastIntegerString
CastCharString
CastDoubleString
CastNatString
CastInt8String
CastInt16String
CastInt32String
CastInt64String
CastBits8String
CastBits16String
CastBits32String
CastBits64String
CastIntInteger
CastCharInteger
CastDoubleInteger
CastStringInteger
CastNatInteger
CastBits8Integer
CastBits16Integer
CastBits32Integer
CastBits64Integer
CastInt8Integer
CastInt16Integer
CastInt32Integer
CastInt64Integer
CastIntegerInt
CastCharInt
CastDoubleInt
CastStringInt
CastNatInt
CastBits8Int
CastBits16Int
CastBits32Int
CastBits64Int
CastInt8Int
CastInt16Int
CastInt32Int
CastInt64Int
CastIntChar
CastIntegerChar
CastNatChar
CastBits8Char
CastBits16Char
CastBits32Char
CastBits64Char
CastInt8Char
CastInt16Char
CastInt32Char
CastInt64Char
CastIntDouble
CastIntegerDouble
CastStringDouble
CastNatDouble
CastBits8Double
CastBits16Double
CastBits32Double
CastBits64Double
CastInt8Double
CastInt16Double
CastInt32Double
CastInt64Double
CastIntBits8
CastIntegerBits8
CastBits16Bits8
CastBits32Bits8
CastBits64Bits8
CastStringBits8
CastDoubleBits8
CastCharBits8
CastNatBits8
CastInt8Bits8
CastInt16Bits8
CastInt32Bits8
CastInt64Bits8
CastIntBits16
CastIntegerBits16
CastBits8Bits16
CastBits32Bits16
CastBits64Bits16
CastStringBits16
CastDoubleBits16
CastCharBits16
CastNatBits16
CastInt8Bits16
CastInt16Bits16
CastInt32Bits16
CastInt64Bits16
CastIntBits32
CastIntegerBits32
CastBits8Bits32
CastBits16Bits32
CastBits64Bits32
CastStringBits32
CastDoubleBits32
CastCharBits32
CastNatBits32
CastInt8Bits32
CastInt16Bits32
CastInt32Bits32
CastInt64Bits32
CastIntBits64
CastIntegerBits64
CastBits8Bits64
CastBits16Bits64
CastBits32Bits64
CastStringBits64
CastDoubleBits64
CastCharBits64
CastNatBits64
CastInt8Bits64
CastInt16Bits64
CastInt32Bits64
CastInt64Bits64
CastStringInt8
CastDoubleInt8
CastCharInt8
CastIntInt8
CastIntegerInt8
CastNatInt8
CastBits8Int8
CastBits16Int8
CastBits32Int8
CastBits64Int8
CastInt16Int8
CastInt32Int8
CastInt64Int8
CastStringInt16
CastDoubleInt16
CastCharInt16
CastIntInt16
CastIntegerInt16
CastNatInt16
CastBits8Int16
CastBits16Int16
CastBits32Int16
CastBits64Int16
CastInt8Int16
CastInt32Int16
CastInt64Int16
CastStringInt32
CastDoubleInt32
CastCharInt32
CastIntInt32
CastIntegerInt32
CastNatInt32
CastBits8Int32
CastBits16Int32
CastBits32Int32
CastBits64Int32
CastInt8Int32
CastInt16Int32
CastInt64Int32
CastStringInt64
CastDoubleInt64
CastCharInt64
CastIntInt64
CastIntegerInt64
CastNatInt64
CastBits8Int64
CastBits16Int64
CastBits32Int64
CastBits64Int64
CastInt8Int64
CastInt16Int64
CastInt32Int64
CastStringNat
CastDoubleNat
CastCharNat
CastIntNat
CastIntegerNat
CastBits8Nat
CastBits16Nat
CastBits32Nat
CastBits64Nat
CastInt8Nat
CastInt16Nat
CastInt32Nat
CastInt64Nat
cast : Castfromto=>from->to
  Perform a (potentially lossy!) cast operation.
@ orig The original type

Totality: total
Visibility: public export