mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-10-26 17:33:47 +03:00
Adjust some tests.
This commit is contained in:
parent
3e398584b3
commit
2d02899679
@ -2,13 +2,13 @@
|
|||||||
000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
|
000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
|
||||||
0000ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 23) (:end 7 25)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
|
0000ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 23) (:end 7 25)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
|
||||||
0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 8 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
|
0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 8 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
|
||||||
0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 38)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:190} a)")))))) 1)
|
0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 38)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:222} a)")))))) 1)
|
||||||
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 11)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:191}_[]")))))) 1)
|
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 11)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:223}_[]")))))) 1)
|
||||||
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:190}_[] ?{_:191}_[])")))))) 1)
|
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:222}_[] ?{_:223}_[])")))))) 1)
|
||||||
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:192}_[] ?{_:191}_[])")))))) 1)
|
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:224}_[] ?{_:223}_[])")))))) 1)
|
||||||
0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 7 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
|
0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 7 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
|
||||||
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:182}_[] ?{_:181}_[])")))))) 1)
|
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:214}_[] ?{_:213}_[])")))))) 1)
|
||||||
0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:172} : (Main.Vect n[0] a[1])) -> (({arg:173} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:630:1--637:1 n[2] m[4]) a[3])))")))))) 1)
|
0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:204} : (Main.Vect n[0] a[1])) -> (({arg:205} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:630:1--637:1 n[2] m[4]) a[3])))")))))) 1)
|
||||||
0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 6 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
|
0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 6 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
|
||||||
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
|
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
|
||||||
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 42)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
|
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 42)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
|
||||||
|
@ -2,13 +2,13 @@
|
|||||||
000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
|
000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
|
||||||
0000ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 23) (:end 7 25)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
|
0000ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 23) (:end 7 25)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
|
||||||
0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 8 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
|
0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 8 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
|
||||||
0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 38)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:190} a)")))))) 1)
|
0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 38)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:222} a)")))))) 1)
|
||||||
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 11)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:191}_[]")))))) 1)
|
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 11)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:223}_[]")))))) 1)
|
||||||
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:190}_[] ?{_:191}_[])")))))) 1)
|
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:222}_[] ?{_:223}_[])")))))) 1)
|
||||||
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:192}_[] ?{_:191}_[])")))))) 1)
|
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:224}_[] ?{_:223}_[])")))))) 1)
|
||||||
0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 7 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
|
0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 7 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
|
||||||
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:182}_[] ?{_:181}_[])")))))) 1)
|
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:214}_[] ?{_:213}_[])")))))) 1)
|
||||||
0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:172} : (Main.Vect n[0] a[1])) -> (({arg:173} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:630:1--637:1 n[2] m[4]) a[3])))")))))) 1)
|
0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:204} : (Main.Vect n[0] a[1])) -> (({arg:205} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:630:1--637:1 n[2] m[4]) a[3])))")))))) 1)
|
||||||
0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 6 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
|
0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 6 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
|
||||||
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
|
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
|
||||||
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 42)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
|
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 42)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
|
||||||
|
@ -1,7 +1,7 @@
|
|||||||
1/1: Building arity (arity.idr)
|
1/1: Building arity (arity.idr)
|
||||||
arity.idr:4:16--4:22:While processing right hand side of foo at arity.idr:4:1--7:1:
|
arity.idr:4:16--4:22:While processing right hand side of foo at arity.idr:4:1--7:1:
|
||||||
When unifying (1 {arg:169} : Nat) -> MyN and MyN
|
When unifying (1 {arg:201} : Nat) -> MyN and MyN
|
||||||
Mismatch between:
|
Mismatch between:
|
||||||
(1 {arg:169} : Nat) -> MyN
|
(1 {arg:201} : Nat) -> MyN
|
||||||
and
|
and
|
||||||
MyN
|
MyN
|
||||||
|
@ -35,4 +35,4 @@ testPerson : Person
|
|||||||
testPerson = MkPerson "Fred" 1337 10 (MkStats 10 10)
|
testPerson = MkPerson "Fred" 1337 10 (MkStats 10 10)
|
||||||
|
|
||||||
grow : Person -> Person
|
grow : Person -> Person
|
||||||
grow = record { more->height $= (+1) }
|
grow = record { more.height $= (+1) }
|
||||||
|
@ -2,5 +2,5 @@ grow testPerson
|
|||||||
grow (grow testPerson)
|
grow (grow testPerson)
|
||||||
cons 10 testPair
|
cons 10 testPair
|
||||||
cons' 10 testPair
|
cons' 10 testPair
|
||||||
record { more -> weight = 94 } testPerson
|
record { more.weight = 94 } testPerson
|
||||||
:q
|
:q
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
module recordname
|
module Recordname
|
||||||
|
|
||||||
namespace Foo
|
namespace Foo
|
||||||
export
|
export
|
||||||
@ -9,4 +9,4 @@ namespace Foo
|
|||||||
x : Name -> Int
|
x : Name -> Int
|
||||||
x = foo
|
x = foo
|
||||||
|
|
||||||
test : recordname.Foo.Name
|
test : Recordname.Foo.Name
|
@ -1 +1 @@
|
|||||||
1/1: Building recordname (recordname.idr)
|
1/1: Building Recordname (Recordname.idr)
|
||||||
|
@ -1,3 +1,3 @@
|
|||||||
$1 recordname.idr --check
|
$1 Recordname.idr --check
|
||||||
|
|
||||||
rm -rf build
|
rm -rf build
|
||||||
|
@ -23,11 +23,11 @@ initState : GameState
|
|||||||
initState = MkGameState (MkScore 0 0) 12
|
initState = MkGameState (MkScore 0 0) 12
|
||||||
|
|
||||||
addWrong : GameState -> GameState
|
addWrong : GameState -> GameState
|
||||||
addWrong = record { score->attempted $= (+1) }
|
addWrong = record { score.attempted $= (+1) }
|
||||||
|
|
||||||
addCorrect : GameState -> GameState
|
addCorrect : GameState -> GameState
|
||||||
addCorrect = record { score->correct $= (+1),
|
addCorrect = record { score.correct $= (+1),
|
||||||
score->attempted $= (+1) }
|
score.attempted $= (+1) }
|
||||||
|
|
||||||
setDifficulty : Int -> GameState -> GameState
|
setDifficulty : Int -> GameState -> GameState
|
||||||
setDifficulty newDiff state = record { difficulty = newDiff } state
|
setDifficulty newDiff state = record { difficulty = newDiff } state
|
||||||
|
Loading…
Reference in New Issue
Block a user