Denis Buzdalov
874496e1ae
[base] Constructor's injectivity proofs for Exists and Subset ( #1118 )
...
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
2021-02-24 19:11:41 +00:00
Denis Buzdalov
69be8f2102
[base] bimap functions were added for dependent pairs.
2021-02-24 16:41:33 +00:00
G. Allais
d2eeb7ce86
[ fix #758 ] desugar non-binding sequencing in do blocks to (>>) ( #1095 )
2021-02-24 11:07:16 +00:00
Guillaume ALLAIS
9be15e7e61
[ re #1106 ] Give more details about directory-related failures
2021-02-23 13:52:20 +00:00
Donovan Crichton
06fe9e3152
[ fix #978 ] Mention Editor Plugins in README ( #1111 )
2021-02-23 11:54:26 +00:00
Mark Barbone
0f7fa149c7
Make zip infixr 6
2021-02-23 10:54:28 +00:00
Denis Buzdalov
95af3cf4be
More compose instances and one usage of them ( #1089 )
2021-02-23 10:53:43 +00:00
Guillaume ALLAIS
00067e8151
[ fix #637 ] force indentation after a with
2021-02-23 10:52:22 +00:00
G. Allais
c10c1d65a5
[ fix #1022 ] detect more impossible cases ( #1108 )
2021-02-23 10:51:38 +00:00
Andy Lok
775d7b4bdb
Add test for escaping NL
2021-02-23 13:10:36 +08:00
Andy Lok
626cfa8e19
Add comment
2021-02-23 02:16:31 +08:00
Andy Lok
2358ac0f73
Fix StrError12 test
2021-02-23 02:10:57 +08:00
Guillaume ALLAIS
741960f0d1
[ test ] case for #484
...
This issue was fixed by #1081
2021-02-22 16:04:04 +00:00
Dong Tsing-hsuen
505224e9fc
[ typo ] Enum -> Range ( #1099 )
2021-02-22 10:05:08 +00:00
Donovan Crichton
1b9a220c42
Added comment descriptions for FC and FilePos.
2021-02-22 09:55:34 +00:00
G. Allais
74b051589b
[ new ] Perfect binary trees ( #1063 )
2021-02-22 09:54:16 +00:00
G. Allais
30d402ed7f
[ fix #899 ] Be careful when generating an impossible LHS ( #1081 )
2021-02-22 09:53:30 +00:00
Mathew Polzin
c3a42966e7
fix indentation in Golden so that prompt happens after both paths under expected and actual outputs don't match.
2021-02-22 09:39:57 +00:00
Andy Lok
2813a68c52
Fix self-host
2021-02-21 03:28:23 +08:00
Andy Lok
83ab4f0f15
Fix lint
2021-02-21 03:13:13 +08:00
Andy Lok
07eb6fda47
Allow hashtag escape for multi-line string
2021-02-21 03:11:01 +08:00
Andy Lok
22a769e6b5
Implement multiline string
2021-02-20 18:05:26 +08:00
Guillaume ALLAIS
7ccc47712e
[ re #1087 ] Better error messages in the REPL
...
(as well as in type signatures now that I know how to do that)
2021-02-19 12:34:19 +00:00
Guillaume ALLAIS
5b5bdfe769
[ contrib ] Positions in strings
...
This is an alternative to using `fastUnpack` and `fastPack` to work
on lists of characters.
Using this to refactor the lexer and benchmarking the resulting
compiler on building idris2 shows it's 3 to 5s slower than the
current implementation that goes via `List Char`.
This may be backend-dependent so I still push this to contrib,
with the plan of running further benchmarks in the future.
2021-02-18 17:52:25 +00:00
Mathew Polzin
d5d0b64b4a
withFile & writeFile cleanup ( #1085 )
2021-02-18 17:51:45 +00:00
Andy Lok
26464357c1
Implement interpolated string ( #1056 )
2021-02-18 13:07:22 +00:00
Mathew Polzin
9f8a8b5d76
Add a total way of reading files in. ( #1070 )
2021-02-18 11:13:25 +00:00
Nil Geisweiller
bb25050746
Remove redundant to
2021-02-18 09:56:42 +00:00
gemmaro
5eafe11de7
A tiny doc fix: the program name was idris
2021-02-17 09:30:52 +00:00
Stiopa Koltsov
1cf9de4021
Hide countFrom function from prelude
...
`countFrom` must have been made public accidentally:
* it is defined in the ranges section of the file, not stream section
* it is used only in `Range` implementation
* the same function `iterate` is defined in `Data.Stream`
```
countFrom start next
```
is the same as
```
iterate next start
```
2021-02-16 19:20:54 +00:00
Johann Rudloff
d86944fca2
Extract findDataFile code from readDataFile and export it
2021-02-16 19:16:07 +00:00
Kamil Shakirov
357e2a4cf6
Use double quotes to display the current working directory
2021-02-16 19:13:52 +00:00
Denis Buzdalov
b355b12cdb
Some cleanup was done. Changed code is mosly equivalent to the former.
...
A lot of useless matches of implicit arguments were removed.
2021-02-16 19:05:33 +00:00
Guillaume ALLAIS
c2532acfd8
[ fix #1035 ] Not an internal error
2021-02-16 17:04:02 +00:00
Guillaume ALLAIS
e9f4dc5252
[ cleanup ] parser long lines
2021-02-16 17:04:02 +00:00
Stefan Hoeck
7401961425
[ new ] Bitwise XOR for Bits64 and Integer ( #1026 )
2021-02-16 15:14:56 +00:00
Denis Buzdalov
0ac34538ec
A function from Not (x = y) to decEq x y = No _ was added.
2021-02-16 12:43:50 +00:00
Nil Geisweiller
f390fba766
Rename Sotrable to Storable
2021-02-16 09:51:44 +00:00
Alex Gryzlov
a1221fdbfd
Document new :l behaviour ( #1061 )
...
Co-authored-by: Kamiλ Shakirov <ska80@users.noreply.github.com>
Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
2021-02-15 18:56:05 +00:00
Dong Tsing-hsuen
447110c686
Fix typo in FC.idr.
...
Change "beeen" to "been".
2021-02-15 17:32:05 +00:00
André Videla
8c7a08f282
Merge pull request #1034 from andylokandy/lexer
...
lexer: add a language-composable tokenizer
2021-02-15 11:45:37 +00:00
Guillaume ALLAIS
059074fe14
[ test ] fix test suite output
2021-02-15 10:35:46 +00:00
Giuseppe Lomurno
440e60a00b
Change PreorderReasoning arguments to 0
2021-02-15 10:35:46 +00:00
Denis Buzdalov
bd21fd51e2
Zero quantities were added to some interface usages.
2021-02-15 10:35:46 +00:00
Andy Lok
ed7ee4a57b
Show more codes in error report
2021-02-15 10:35:46 +00:00
Michael Messer
0a76ab590e
Generalize Category
2021-02-15 10:35:46 +00:00
G. Allais
301324b9b3
[ fix #1043 ] throw error if compileExpr failed ( #1052 )
...
Also adding a CI target testing the gambit backend.
2021-02-15 10:35:46 +00:00
russoul
1d23c7a6bd
Add named instances for functor & applicative composition
2021-02-15 10:35:46 +00:00
G. Allais
a060dcc18e
[ new ] Data.OpenUnion ( #1050 )
2021-02-15 10:35:46 +00:00
Z-snails
5384560009
[ new ] support record projections in refc backend ( #1054 )
2021-02-15 10:35:46 +00:00
