mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-19 09:12:34 +03:00
26 lines
823 B
Plaintext
26 lines
823 B
Plaintext
1/1: Building TypeSearch (TypeSearch.idr)
|
|
Main> prim__cast_CharString : Char -> String
|
|
Main.sameSig : Char -> String
|
|
Visibility: private
|
|
Data.String.singleton : Char -> String
|
|
Totality: total
|
|
Visibility: public export
|
|
Prelude.Show.show : Char -> String
|
|
Prelude.Cast.cast : Char -> String
|
|
Main> Prelude.const : a -> b -> a
|
|
Constant function. Ignores its second argument.
|
|
Totality: total
|
|
Visibility: public export
|
|
Main> Builtin.fromChar : Char -> Char
|
|
Prelude.toUpper : Char -> Char
|
|
Convert a letter to the corresponding upper-case letter, if any.
|
|
Non-letters are ignored.
|
|
Totality: total
|
|
Visibility: public export
|
|
Prelude.toLower : Char -> Char
|
|
Convert a letter to the corresponding lower-case letter, if any.
|
|
Non-letters are ignored.
|
|
Totality: total
|
|
Visibility: public export
|
|
Main> Bye for now!
|