Idris2Doc : Literal.Prelude

Literal.Prelude

(source)
This provides `Lit` implementations for the types from the
prelude. If you import this, make sure to add the following
pragmas to the top of your source files:

```idris
%hide Builtin.fromString
%hide Builtin.fromChar
%hide Builtin.fromInteger
%hide Builtin.fromDouble
```

Even then, you might experience some interference when using
other libraries or data types. Only use if you know what you
are doing.

Reexports

import public Literal

Definitions

stringLitImpl : StringLit String
Totality: total
Visibility: public export
charLitImpl : CharLit Char
Totality: total
Visibility: public export
doubleLitImpl : DoubleLit Double
Totality: total
Visibility: public export
integerLitImpl : IntegerLit Integer
Totality: total
Visibility: public export
intLitImpl : IntegerLit Int
Totality: total
Visibility: public export
natLitImpl : IntegerLit Nat
Totality: total
Visibility: public export
bits8LitImpl : IntegerLit Bits8
Totality: total
Visibility: public export
bits16LitImpl : IntegerLit Bits16
Totality: total
Visibility: public export
bits32LitImpl : IntegerLit Bits32
Totality: total
Visibility: public export
bits64LitImpl : IntegerLit Bits64
Totality: total
Visibility: public export
int8LitImpl : IntegerLit Int8
Totality: total
Visibility: public export
int16LitImpl : IntegerLit Int16
Totality: total
Visibility: public export
int32LitImpl : IntegerLit Int32
Totality: total
Visibility: public export
int64LitImpl : IntegerLit Int64
Totality: total
Visibility: public export