Literal

(source)

Definitions

interface CharLit : Type -> Type

Parameters: a
Constructor:

CL

Methods:

0 CharPred : Char -> Type
fromChar : (c : Char) -> {auto 0 _ : CharPred c} -> a

Implementation:

Cast Char a => CharLit (Subset a p)

0 CharPred : CharLit a => Char -> Type

Totality: total
Visibility: public export

fromChar : {auto __con : CharLit a} -> (c : Char) -> {auto 0 _ : CharPred c} -> a

Totality: total
Visibility: public export

interface DoubleLit : Type -> Type

Parameters: a
Constructor:

DL

Methods:

0 DoublePred : Double -> Type
fromDouble : (d : Double) -> {auto 0 _ : DoublePred d} -> a

Implementation:

Cast Double a => DoubleLit (Subset a p)

0 DoublePred : DoubleLit a => Double -> Type

Totality: total
Visibility: public export

fromDouble : {auto __con : DoubleLit a} -> (d : Double) -> {auto 0 _ : DoublePred d} -> a

Totality: total
Visibility: public export

interface IntegerLit : Type -> Type

Parameters: a
Constructor:

IL

Methods:

0 IntegerPred : Integer -> Type
fromInteger : (i : Integer) -> {auto 0 _ : IntegerPred i} -> a

Implementation:

Cast Integer a => IntegerLit (Subset a p)

0 IntegerPred : IntegerLit a => Integer -> Type

Totality: total
Visibility: public export

fromInteger : {auto __con : IntegerLit a} -> (i : Integer) -> {auto 0 _ : IntegerPred i} -> a

Totality: total
Visibility: public export

interface StringLit : Type -> Type

Parameters: a
Constructor:

SL

Methods:

0 StringPred : String -> Type
fromString : (s : String) -> {auto 0 _ : StringPred s} -> a

Implementation:

Cast String a => StringLit (Subset a p)

0 StringPred : StringLit a => String -> Type

Totality: total
Visibility: public export

fromString : {auto __con : StringLit a} -> (s : String) -> {auto 0 _ : StringPred s} -> a

Totality: total
Visibility: public export

mkIL : (p : (Integer -> Type)) -> ((i : Integer) -> (0 _ : p i) -> a) -> IntegerLit a

Totality: total
Visibility: public export

mkSL : (p : (String -> Type)) -> ((i : String) -> (0 _ : p i) -> a) -> StringLit a

Totality: total
Visibility: public export

mkCL : (p : (Char -> Type)) -> ((i : Char) -> (0 _ : p i) -> a) -> CharLit a

Totality: total
Visibility: public export

mkDL : (p : (Double -> Type)) -> ((i : Double) -> (0 _ : p i) -> a) -> DoubleLit a

Totality: total
Visibility: public export

ilPlain : (Integer -> a) -> IntegerLit a

Totality: total
Visibility: public export

clPlain : (Char -> a) -> CharLit a

Totality: total
Visibility: public export

slPlain : (String -> a) -> StringLit a

Totality: total
Visibility: public export

dlPlain : (Double -> a) -> DoubleLit a

Totality: total
Visibility: public export