c486513 · Idris-dev · git.iko.soy

CHANGELOG+4

compare with master

unifiedsplit

@@ -3,6 +3,10 @@ New in 0.9.11:

3

4* Agda-style equational reasoning (in Syntax.PreorderReasoning)

5* 'case' construct now abstracts over the scrutinee in its type

6+* Added label type 'name (equivalent to the empty type).

7+ This is intended for field/effect disambiguation. "name" can be any

8+ valid identifier. Two labels are definitionally equal if they have the

9+ same name.

6

10

7New in 0.9.10:

11New in 0.9.10:

8--------------

12--------------

libs/prelude/Builtins.idr+3

@@ -12,6 +12,9 @@ getProof (a ** v) = v

12

13FalseElim : _|_ -> a

14

15+-- For 'symbol syntax. 'foo becomes Symbol_ "foo"

16+data Symbol_ : String -> Type where

17+

15-- ------------------------------------------------------ [ For rewrite tactic ]

18-- ------------------------------------------------------ [ For rewrite tactic ]

16replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y

19replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y

17replace refl prf = prf

20replace refl prf = prf

src/Idris/ParseExpr.hs+6−3

@@ -287,9 +287,12 @@ simpleExpr syn =

287 <|> tacticsExpr syn

288 <|> caseExpr syn

289 <|> do reserved "Type"; return PType

290− <|> do c <- constant

290+ <|> try (do c <- constant

291− fc <- getFC

291+ fc <- getFC

292− return (modifyConst syn fc (PConstant c))

292+ return (modifyConst syn fc (PConstant c)))

293+ <|> try (do symbol "'"; fc <- getFC; str <- name

294+ return (PApp fc (PRef fc (UN "Symbol_"))

295+ [pexp (PConstant (Str (show str)))]))

293 <|> do fc <- getFC

296 <|> do fc <- getFC

294 x <- fnName

297 x <- fnName

295 return (PRef fc x)

298 return (PRef fc x)