mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-09-11 21:37:48 +03:00
[ new ] Add FromChar
and FromDouble
interfaces to the prelude (#1641)
This commit is contained in:
parent
35638048a3
commit
f5bcc81115
@ -230,3 +230,47 @@ FromString String where
|
||||
public export
|
||||
defaultString : FromString String
|
||||
defaultString = %search
|
||||
|
||||
%charLit fromChar
|
||||
|
||||
||| Interface for types that can be constructed from char literals.
|
||||
public export
|
||||
interface FromChar ty where
|
||||
constructor MkFromChar
|
||||
||| Conversion from Char.
|
||||
fromChar : Char -> ty
|
||||
|
||||
%allow_overloads fromChar
|
||||
|
||||
%inline
|
||||
public export
|
||||
FromChar Char where
|
||||
fromChar s = s
|
||||
|
||||
%defaulthint
|
||||
%inline
|
||||
public export
|
||||
defaultChar : FromChar Char
|
||||
defaultChar = %search
|
||||
|
||||
%doubleLit fromDouble
|
||||
|
||||
||| Interface for types that can be constructed from double literals.
|
||||
public export
|
||||
interface FromDouble ty where
|
||||
constructor MkFromDouble
|
||||
||| Conversion from Double.
|
||||
fromDouble : Double -> ty
|
||||
|
||||
%allow_overloads fromDouble
|
||||
|
||||
%inline
|
||||
public export
|
||||
FromDouble Double where
|
||||
fromDouble s = s
|
||||
|
||||
%defaulthint
|
||||
%inline
|
||||
public export
|
||||
defaultDouble : FromDouble Double
|
||||
defaultDouble = %search
|
||||
|
@ -1,14 +1,5 @@
|
||||
import Data.So
|
||||
|
||||
%doubleLit fromDouble
|
||||
|
||||
public export
|
||||
interface FromDouble ty where
|
||||
fromDouble : Double -> ty
|
||||
|
||||
%allow_overloads fromDouble
|
||||
|
||||
|
||||
record Newtype where
|
||||
constructor
|
||||
MkNewtype
|
||||
|
@ -30,7 +30,7 @@ Issue1031-3:4:6--4:7
|
||||
|
||||
1/1: Building Issue1031-4 (Issue1031-4.idr)
|
||||
Error: While processing left hand side of nice. Unsolved holes:
|
||||
Main.{dotTm:335} introduced at:
|
||||
Main.{dotTm:373} introduced at:
|
||||
Issue1031-4:4:6--4:10
|
||||
1 | %default total
|
||||
2 |
|
||||
|
@ -13,7 +13,9 @@ Prelude.Cast.cast : Char -> String
|
||||
Main> Prelude.const : a -> b -> a
|
||||
Constant function. Ignores its second argument.
|
||||
Totality: total
|
||||
Main> Prelude.toUpper : Char -> Char
|
||||
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
|
||||
|
@ -35,7 +35,7 @@ refprims:49:10--49:25
|
||||
49 | dummy3 = %runElab logBad
|
||||
^^^^^^^^^^^^^^^
|
||||
|
||||
Error: While processing right hand side of dummy4. Error during reflection: failed after generating Main.{plus:XXX}
|
||||
Error: While processing right hand side of dummy4. Error during reflection: failed after generating Main.{plus:XXXX}
|
||||
|
||||
refprims:52:10--52:28
|
||||
48 | dummy3 : a
|
||||
|
Loading…
Reference in New Issue
Block a user