edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-11-28 05:32:03 +03:00
Code Issues Projects Releases Wiki Activity

Update tests/idris2/literate012/expected

Browse Source 
Co-Authored-By: G. Allais <guillaume.allais@ens-lyon.org>
This commit is contained in:
Jan de Muijnck-Hughes 2020-04-22 20:37:07 +01:00 committed by GitHub
parent 0e73bf976b
commit e091ca5701
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
tests/idris2/literate012/expected
View File

@ -1,5 +1,5 @@
1/1: Building IEdit (IEdit.org)
Main> append {n = Z} [] ys = ?foo_1
Main> append {n = 0} [] ys = ?foo_1
append {n = (S k)} (x :: xs) ys = ?foo_2
Main> vadd [] [] = ?bar_1
Main> vadd (x :: xs) (y :: ys) = ?baz_1