git.iko.soy/Idris-dev
on master help sign in
Added record test
d54f335Edwin Brady
CHANGELOG+1−1
compare with master
unifiedsplit
@@ -4,7 +4,7 @@ New in 0.9.1:
4User visible changes:
4User visible changes:
5
5
6* dsl notation
6* dsl notation
7−* record projection
7+* record projection and update
8* auto implicits and default argument values {auto n : T}, {default val n : T}
8* auto implicits and default argument values {auto n : T}, {default val n : T}
9* Additions to prelude
9* Additions to prelude
10
10
test/README+2
@@ -9,3 +9,5 @@ Tests:
9007: Applicative and idiom brackets
9007: Applicative and idiom brackets
10008: case and pattern matching let
10008: case and pattern matching let
11009: ranges and list monad
11009: ranges and list monad
12+010: total
13+011: record projection and update
test/test011/expectednew file+5
@@ -0,0 +1,5 @@
1+foo
2+Fred
3+[1, 2, 3]
4+[b, a]
5+25
test/test011/runnew file+4
@@ -0,0 +1,4 @@
1+#!/bin/bash
2+idris test011.idr -o test011
3+./test011
4+rm -f test011 test011.ibc
test/test011/test011.idrnew file+26
@@ -0,0 +1,26 @@
1+module main
2+
3+record Foo : Nat -> Set where
4+ MkFoo : (name : String) ->
5+ (things : Vect a n) ->
6+ (more_things : Vect b m) ->
7+ Foo n
8+
9+record Person : Set where
10+ MkPerson : (name : String) -> (age : Int) -> Person
11+
12+testFoo : Foo 3
13+testFoo = MkFoo "name" [1,2,3] [4,5,6,7]
14+
15+person : Person
16+person = MkPerson "Fred" 30
17+
18+main : IO ()
19+main = do let x = record { name = "foo",
20+ more_things = reverse ["a","b"] } testFoo
21+ print $ name x
22+ print $ name person
23+ print $ things x
24+ print $ more_things x
25+ print $ age (record { age = 25 } person)
26+