Prelude.Cast

Definitions

interface Cast : 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:

Cast a a

Cast Int String

Cast Integer String

Cast Char String

Cast Double String

Cast Nat String

Cast Int8 String

Cast Int16 String

Cast Int32 String

Cast Int64 String

Cast Bits8 String

Cast Bits16 String

Cast Bits32 String

Cast Bits64 String

Cast Int Integer

Cast Char Integer

Cast Double Integer

Cast String Integer

Cast Nat Integer

Cast Bits8 Integer

Cast Bits16 Integer

Cast Bits32 Integer

Cast Bits64 Integer

Cast Int8 Integer

Cast Int16 Integer

Cast Int32 Integer

Cast Int64 Integer

Cast Integer Int

Cast Char Int

Cast Double Int

Cast String Int

Cast Nat Int

Cast Bits8 Int

Cast Bits16 Int

Cast Bits32 Int

Cast Bits64 Int

Cast Int8 Int

Cast Int16 Int

Cast Int32 Int

Cast Int64 Int

Cast Int Char

Cast Integer Char

Cast Nat Char

Cast Bits8 Char

Cast Bits16 Char

Cast Bits32 Char

Cast Bits64 Char

Cast Int8 Char

Cast Int16 Char

Cast Int32 Char

Cast Int64 Char

Cast Int Double

Cast Integer Double

Cast String Double

Cast Nat Double

Cast Bits8 Double

Cast Bits16 Double

Cast Bits32 Double

Cast Bits64 Double

Cast Int8 Double

Cast Int16 Double

Cast Int32 Double

Cast Int64 Double

Cast Int Bits8

Cast Integer Bits8

Cast Bits16 Bits8

Cast Bits32 Bits8

Cast Bits64 Bits8

Cast String Bits8

Cast Double Bits8

Cast Char Bits8

Cast Nat Bits8

Cast Int8 Bits8

Cast Int16 Bits8

Cast Int32 Bits8

Cast Int64 Bits8

Cast Int Bits16

Cast Integer Bits16

Cast Bits8 Bits16

Cast Bits32 Bits16

Cast Bits64 Bits16

Cast String Bits16

Cast Double Bits16

Cast Char Bits16

Cast Nat Bits16

Cast Int8 Bits16

Cast Int16 Bits16

Cast Int32 Bits16

Cast Int64 Bits16

Cast Int Bits32

Cast Integer Bits32

Cast Bits8 Bits32

Cast Bits16 Bits32

Cast Bits64 Bits32

Cast String Bits32

Cast Double Bits32

Cast Char Bits32

Cast Nat Bits32

Cast Int8 Bits32

Cast Int16 Bits32

Cast Int32 Bits32

Cast Int64 Bits32

Cast Int Bits64

Cast Integer Bits64

Cast Bits8 Bits64

Cast Bits16 Bits64

Cast Bits32 Bits64

Cast String Bits64

Cast Double Bits64

Cast Char Bits64

Cast Nat Bits64

Cast Int8 Bits64

Cast Int16 Bits64

Cast Int32 Bits64

Cast Int64 Bits64

Cast String Int8

Cast Double Int8

Cast Char Int8

Cast Int Int8

Cast Integer Int8

Cast Nat Int8

Cast Bits8 Int8

Cast Bits16 Int8

Cast Bits32 Int8

Cast Bits64 Int8

Cast Int16 Int8

Cast Int32 Int8

Cast Int64 Int8

Cast String Int16

Cast Double Int16

Cast Char Int16

Cast Int Int16

Cast Integer Int16

Cast Nat Int16

Cast Bits8 Int16

Cast Bits16 Int16

Cast Bits32 Int16

Cast Bits64 Int16

Cast Int8 Int16

Cast Int32 Int16

Cast Int64 Int16

Cast String Int32

Cast Double Int32

Cast Char Int32

Cast Int Int32

Cast Integer Int32

Cast Nat Int32

Cast Bits8 Int32

Cast Bits16 Int32

Cast Bits32 Int32

Cast Bits64 Int32

Cast Int8 Int32

Cast Int16 Int32

Cast Int64 Int32

Cast String Int64

Cast Double Int64

Cast Char Int64

Cast Int Int64

Cast Integer Int64

Cast Nat Int64

Cast Bits8 Int64

Cast Bits16 Int64

Cast Bits32 Int64

Cast Bits64 Int64

Cast Int8 Int64

Cast Int16 Int64

Cast Int32 Int64

Cast String Nat

Cast Double Nat

Cast Char Nat

Cast Int Nat

Cast Integer Nat

Cast Bits8 Nat

Cast Bits16 Nat

Cast Bits32 Nat

Cast Bits64 Nat

Cast Int8 Nat

Cast Int16 Nat

Cast Int32 Nat

Cast Int64 Nat

cast : Cast from to => from -> to

  Perform a (potentially lossy!) cast operation.
  @ orig The original type

Totality: total
Visibility: public export