idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-22 03:01:31 +03:00
Code Issues Projects Releases Wiki Activity
1,071 Commits 6 Branches 9 Tags 115 MiB
3a7b72f384
Commit Graph

295 Commits

Author SHA1 Message Date
Thomas Dziedzic
a7ff5aa71f
implement HVect (#563) 2020-08-26 15:48:19 +01:00
russoul
3a9b1ac656 Add supporting code 2020-08-25 14:30:57 +03:00
russoul
50ac934747 Merge branch 'master' of https://github.com/idris-lang/Idris2 into master 2020-08-25 13:57:26 +03:00
MarcelineVQ
209de36ba0
add EitherT transformer (#590) 
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
 2020-08-25 11:14:09 +01:00
Matus Tejiscak
f69443985b Revert addition to ES preamble. 2020-08-25 10:25:45 +02:00
Matus Tejiscak
e9e5ef3d6a Fix FFI specifier. 2020-08-25 10:23:07 +02:00
Matus Tejiscak
1eaecc5d66 Implement stringConcat in Node. 2020-08-25 09:46:35 +02:00
Matus Tejiscak
969a6e1a45 Make fastAppend a deprecated alias of fastConcat. 2020-08-24 19:51:23 +02:00
Matus Tejiscak
362d2204ab Make fastAppend a foreign call. 2020-08-24 19:51:22 +02:00
russoul
594105d5ac Eliminate schemeCall from the library 2020-08-24 19:38:29 +03:00
Alex Gryzlov
ef5299733a
refactor Data.String.Parser (#579) 2020-08-22 08:13:34 +01:00
G. Allais
da78ac4783
[ new ] topics for logging levels (#569) 2020-08-20 18:45:34 +01:00
Cole Brown
f227735cec Add local to MonadReader interface 2020-08-20 16:33:50 +01:00
Cole Brown
6c3ab219bc Implement MonadReader and related types/instances 
This includes:
- ReaderT transformer
- Instances for Functor, Applicative, Monad, MonadTrans, HasIO,
  Alternative
- asks helper function
- Reader alias
 2020-08-20 16:33:50 +01:00
karroffel
7d046652d8
add support for more casts from and to BitsN types (#548) 
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
 2020-08-20 15:01:09 +01:00
Thomas Dziedzic
5d1b937035
add prim__getNullAnyPtr and prim__castPtr (#525) 2020-08-20 11:52:51 +01:00
Ohad Kammar
310b7a007c Move cong2 from contrib to Prelude.Basics 2020-08-20 07:53:45 +01:00
Ohad Kammar
080fbab20d Insert linearity annotations for cong2 
following review by @gallais
 2020-08-20 07:53:45 +01:00
Kamil Shakirov
8544e80076 Use the same naming convention for foreign primitives 2020-08-19 14:05:28 +01:00
Arnaud Bailly
8ecf664ff6
Port Decidable.Order from Idris1 (#543) 2020-08-18 22:26:56 +01:00
Giuseppe Lomurno
df4f990b3c PTerm and error intial prettyprinting 2020-08-18 19:25:36 +01:00
Niklas Larsson
76ee7a3b34
Merge pull request #351 from petithug/fixity-precedence-master 
Restore Bool operators precedence
 2020-08-18 14:08:20 +02:00
Niklas Larsson
84ae9d7c6e
Merge pull request #523 from mb64/hasio-statet 
Implement HasIO for StateT
 2020-08-18 14:02:02 +02:00
Niklas Larsson
93ecb72012
Merge pull request #526 from alexhumphreys/feat/buildExpressionParser 
Add BuildExpressionParser to contrib
 2020-08-18 14:01:20 +02:00
Ohad Kammar
10b8698843 Remove forgotten linearity annotation on cong2 2020-08-16 08:20:31 +01:00
Ohad Kammar
d82a3e0e42 contrib: Add a 2-holed congruence function 
For lack of a better place, I've put it in `Syntax.PreorderReasoning`

These equations are natural in equational reasoning, but less so when
rewriting, so that's why it's there
 2020-08-16 08:20:31 +01:00
Alex Humphreys
f47d9cfef2 Add integer paser and extra test 
Signed-off-by: Alex Humphreys <alex.humphreys@here.com>
 2020-08-10 13:26:20 +02:00
Alex Humphreys
f020fd29e8 Use overloaded Fin literals 
Signed-off-by: Alex Humphreys <alex.humphreys@here.com>
 2020-08-10 13:26:20 +02:00
Thomas Dziedzic
a1739a69a0
Update app docs (#537) 2020-08-10 10:05:23 +01:00
Ohad Kammar
7f960ed938 Remove bindning to y as no longer necessary 2020-08-09 10:18:34 +01:00
Ohad Kammar
ff76dee6c7 Try a fix for the preorder reasoning error 
Correct the dependency in `FastDerivation` to use the RHS in `step`
Try to avoid shadowing `y` in the LHS of `Calc`
 2020-08-09 10:18:34 +01:00
russoul
d387c76e9b update stdio docs 2020-08-08 12:49:33 +01:00
Alex Humphreys
d4cbb8a620 Move natural and digit combinators 
Signed-off-by: Alex Humphreys <alex.humphreys@here.com>
 2020-08-07 19:20:32 +02:00
Alex Humphreys
40427bd527 Move combinators to Data.String.Parser 2020-08-06 13:16:47 +02:00
Alex Humphreys
97b41d1ad9 Rename BuildExpressionParser to Parser.Expression 
Signed-off-by: Alex Humphreys <alex.humphreys@here.com>
 2020-08-06 12:42:38 +02:00
Alex Humphreys
22915d23ca Remove LO function 
Signed-off-by: Alex Humphreys <alex.humphreys@here.com>
 2020-08-06 12:27:42 +02:00
Alex Humphreys
eca083cdcc Add License comment to BuildExpressionParser 
Signed-off-by: Alex Humphreys <alex.humphreys@here.com>
 2020-08-06 08:59:57 +02:00
Alex Humphreys
29e49a74c5 Add BuildExpressionParser to contrib 
Signed-off-by: Alex Humphreys <alex.humphreys@here.com>
 2020-08-06 08:59:57 +02:00
Giuseppe Lomurno
723457fd6c Remove public export 2020-08-05 13:42:04 +02:00
Giuseppe Lomurno
c28133b7d9 Renamed IsString to FromString 
- Renaming of the string overload interface
- Added test cases for both string and integer literals overload
 2020-08-05 02:33:05 +02:00
Giuseppe Lomurno
b7ba5e88eb Overloaded strings interface 
As for integer literals, adds an interface for overloaded string
literals, and the implementation for the prettyprinter library in
contrib.
 2020-08-05 02:00:05 +02:00
Mark Barbone
10d28efd52
Implement HasIO for StateT 2020-08-04 17:19:45 -04:00
G. Allais
0a7ea69df5
[ refactor ] introduce List1 to remove impossible case (#520) 2020-08-04 20:03:18 +01:00
Edwin Brady
2761a27357
Merge pull request #476 from nickdrozd/algebra-implementations 
Add some algebra implementations
 2020-08-04 13:21:12 +01:00
Mark Barbone
cef248e5a7 Make showParens public 2020-08-04 10:58:00 +01:00
Ohad Kammar
5cfbac4a51 Add irrelevance annotations to Data.List functions taking NonEmpty 2020-07-30 06:01:42 +01:00
Alex Gryzlov
69612bf6bf
Add list lemmas (#491) 2020-07-29 10:51:07 +01:00
Ohad Kammar
915b7bea38 Add various instances from stdlib interfaces (Eq, Ord, DecEq) 
For Void and Either

This is because I ended up using them elsewhere, so why not include them in the stdlib.

Also expose left/rightInjective functions, as are used in the DecEq proofs.
 2020-07-26 10:47:38 +01:00
Giuseppe Lomurno
39f23ffd9b Prec version of pretty interface 2020-07-24 15:19:17 +01:00
Giuseppe Lomurno
ab1f383912 Laziness annotations for performance 2020-07-24 15:19:17 +01:00