mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-27 13:40:15 +03:00
Bring #1719 up to date with latest changes
This commit is contained in:
parent
4079ae0e25
commit
f51aa22046
@ -423,6 +423,7 @@ jsOp StrSubstr [offset, len, str] =
|
||||
pure $ callFun (esName "substr") [offset,len,str]
|
||||
jsOp DoubleExp [x] = pure $ callFun1 "Math.exp" x
|
||||
jsOp DoubleLog [x] = pure $ callFun1 "Math.log" x
|
||||
jsOp DoublePow [x, y] = pure $ callFun "Math.pow" [x, y]
|
||||
jsOp DoubleSin [x] = pure $ callFun1 "Math.sin" x
|
||||
jsOp DoubleCos [x] = pure $ callFun1 "Math.cos" x
|
||||
jsOp DoubleTan [x] = pure $ callFun1 "Math.tan" x
|
||||
|
@ -1,5 +1,4 @@
|
||||
cd "folder with spaces" || exit
|
||||
rm -rf build
|
||||
|
||||
cd "folder with spaces" || exit
|
||||
|
||||
$1 --no-color --console-width 0 --no-banner Main.idr < ../input
|
||||
|
@ -1,10 +1,10 @@
|
||||
1/1: Building Name (Name.idr)
|
||||
LOG declare.data:1: Processing Main.Identity
|
||||
LOG declare.type:1: Processing Main.nested
|
||||
LOG declare.type:1: Processing Main.2963:747:foo
|
||||
LOG declare.type:1: Processing Main.2964:747:foo
|
||||
LOG declare.type:1: Processing Main.cased
|
||||
LOG declare.type:1: Processing Main.test
|
||||
LOG 1: nested: ((Main.MkIdentity [a = Int]) Main.2963:747:foo)
|
||||
LOG 1: nested: ((Main.MkIdentity [a = Int]) Main.2964:747:foo)
|
||||
LOG 1: True
|
||||
LOG 1: cased: (%lam RigW Explicit (Just {lamc:0}) (Main.Identity Int) (Main.case block in cased {lamc:0}))
|
||||
LOG 1: 10
|
||||
|
@ -2,5 +2,5 @@ Processing as TTImp
|
||||
Written TTC
|
||||
Yaffle> ((Main.Just [a = ((Main.Vect.Vect (Main.S Main.Z)) Integer)]) ((((Main.Vect.Cons [k = Main.Z]) [a = Integer]) 1) (Main.Vect.Nil [a = Integer])))
|
||||
Yaffle> ((Main.MkInfer [a = (Main.List.List Integer)]) (((Main.List.Cons [a = Integer]) 1) (Main.List.Nil [a = Integer])))
|
||||
Yaffle> (Interactive):1:9--1:12:Ambiguous elaboration [($resolved381 ?Main.{a:59}_[]), ($resolved362 ?Main.{a:59}_[])]
|
||||
Yaffle> (Interactive):1:9--1:12:Ambiguous elaboration [($resolved382 ?Main.{a:59}_[]), ($resolved363 ?Main.{a:59}_[])]
|
||||
Yaffle> Bye for now!
|
||||
|
@ -2,7 +2,7 @@ Processing as TTImp
|
||||
Written TTC
|
||||
Yaffle> Bye for now!
|
||||
Processing as TTImp
|
||||
Vect2:25:1--26:1:{pat 0 {b:28} : Type} => {pat 0 {a:27} : Type} => ($resolved380 {b:28}[1] {a:27}[0] $resolved361 ($resolved370 {a:27}[0]) ($resolved370 {b:28}[1])) is not a valid impossible pattern because it typechecks
|
||||
Vect2:25:1--26:1:{pat 0 {b:28} : Type} => {pat 0 {a:27} : Type} => ($resolved381 {b:28}[1] {a:27}[0] $resolved362 ($resolved371 {a:27}[0]) ($resolved371 {b:28}[1])) is not a valid impossible pattern because it typechecks
|
||||
Yaffle> Bye for now!
|
||||
Processing as TTImp
|
||||
Vect3:25:1--26:1:Not a valid impossible pattern:
|
||||
|
@ -2,6 +2,6 @@ Processing as TTImp
|
||||
Written TTC
|
||||
Yaffle> Main.lookup: All cases covered
|
||||
Yaffle> Main.lookup':
|
||||
($resolved409 [__] [__] ($resolved377 [__]) {_:60})
|
||||
($resolved410 [__] [__] ($resolved378 [__]) {_:60})
|
||||
Yaffle> Main.lookup'': Calls non covering function Main.lookup'
|
||||
Yaffle> Bye for now!
|
||||
|
@ -3,13 +3,13 @@ Written TTC
|
||||
Yaffle> Bye for now!
|
||||
Processing as TTImp
|
||||
Dot2:15:1--16:1:When elaborating left hand side of Main.half:
|
||||
Dot2:15:28--15:30:Pattern variable {P:n:365} unifies with ?{P:m:365}_[]
|
||||
Dot2:15:28--15:30:Pattern variable {P:n:366} unifies with ?{P:m:366}_[]
|
||||
Yaffle> Bye for now!
|
||||
Processing as TTImp
|
||||
Dot3:18:1--19:1:When elaborating left hand side of Main.addBaz3:
|
||||
Dot3:18:10--18:15:Can't match on ($resolved357 ?{P:x:370}_[] ?{P:x:370}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved357 ?Main.{_:13}_[] ?Main.{_:14}_[])
|
||||
Dot3:18:10--18:15:Can't match on ($resolved358 ?{P:x:371}_[] ?{P:x:371}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved358 ?Main.{_:13}_[] ?Main.{_:14}_[])
|
||||
Yaffle> Bye for now!
|
||||
Processing as TTImp
|
||||
Dot4:17:1--18:1:When elaborating left hand side of Main.addBaz4:
|
||||
Dot4:17:33--17:34:Can't match on ?{P:x:372}_[] (Non linear pattern variable) - it elaborates to ?Main.{dotTm:15}_[]
|
||||
Dot4:17:33--17:34:Can't match on ?{P:x:373}_[] (Non linear pattern variable) - it elaborates to ?Main.{dotTm:15}_[]
|
||||
Yaffle> Bye for now!
|
||||
|
Loading…
Reference in New Issue
Block a user