idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-09-21 02:07:25 +03:00
Code Issues Projects Releases Wiki Activity

Update literate test results

Browse Source 
New search heuristic finds a slightly better zipWith, in particular.
This commit is contained in:
Edwin Brady 2020-07-30 00:08:06 +01:00
parent 8d7fa5c642
commit ff48bb2310
3 changed files with 4 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
tests/idris2/literate003/expected
View File

@ -6,7 +6,7 @@ Main> > append [] ys = ys
> append (x :: xs) ys = x :: append xs ys
Main> > lappend [] ys = ys
> lappend (x :: xs) ys = x :: lappend xs ys
Main> > zipWith f [] ys = []
Main> > zipWith f [] [] = []
> zipWith f (x :: xs) (y :: ys) = f x y :: zipWith f xs ys
Main> > lookup Here (ECons x es) = x
> lookup (There p) (ECons x es) = lookup p es

4
tests/idris2/literate007/expected
View File

@ -1,8 +1,8 @@
1/1: Building IEdit (IEdit.lidr)
Main> > zipHere [] ys = []
Main> > zipHere [] [] = []
> zipHere (x :: xs) (y :: ys) = (x, y) :: zipHere xs ys
Main> Bye for now!
1/1: Building IEditOrg (IEditOrg.org)
Main> #+IDRIS: zipHere [] ys = []
Main> #+IDRIS: zipHere [] [] = []
#+IDRIS: zipHere (x :: xs) (y :: ys) = (x, y) :: zipHere xs ys
Main> Bye for now!

2
tests/idris2/literate011/expected
View File

@ -1,4 +1,4 @@
1/1: Building IEdit (IEdit.md)
Main> zipHere [] ys = []
Main> zipHere [] [] = []
zipHere (x :: xs) (y :: ys) = (x, y) :: zipHere xs ys
Main> Bye for now!