Edwin Brady
3794b20d0c
Normalise to / in generating interface names
...
In practice, this is only for consistency in the tests. Is this the
right way?
2020-07-12 17:33:33 +01:00
Edwin Brady
6a53e0177c
Reorganise prelude into multiple files
...
This is partly to tidy things up, but also a good test for 'import as'.
Requires some internal changes since there are parts of reflection,
unelaboration and a compiler hack that rely on where things are in the
Prelude.
2020-07-12 16:55:48 +01:00
Edwin Brady
9d6f365ad7
Merge github.com:idris-lang/Idris2
2020-07-12 12:49:15 +01:00
Edwin Brady
183bac8667
Update namespaces with aliases in output
2020-07-12 12:48:48 +01:00
Niklas Larsson
fb481cd2d1
Merge pull request #448 from melted/simplify_ipkg
...
Make the idris2 executable depend on the idris2 lib
2020-07-11 11:01:47 +02:00
Edwin Brady
b3bb73cfd6
Merge pull request #455 from edwinb/export-nat-prfs
...
Data.Nat proofs should be exported
2020-07-10 23:30:09 +01:00
Edwin Brady
58e28170ac
Data.Nat proofs should be exported
...
I assumed these were copied directly from the Idris 1 libraries, where
there was an %access directive that we don't have any more.
2020-07-10 22:59:46 +01:00
Jan de Muijnck-Hughes
5774a9c6ae
If we know the types of a
& b
start searching.
...
This is helpful when defining auto-implicits of the form:
pairEqF : DecEq a
=> (thisX, x, y : a)
-> {prfRefl : Equal x thisX}
-> (prfEq : decEq x thisX = Yes prfRefl)
=> Pair a a
pairEqF thisX x y {prfRefl} {prfEq} = MkPair x y
before auto-implicit search would fail to find `Refl` for `prfRefl`.
With this fix the solution is found.
This fix means we can avoid having to write the following.
pairEqF' : DecEq a
=> (thisX, x, y : a)
-> (prfEq : decEq x thisX = Yes (the (Equal x x) Refl))
=> Pair a a
pairEqF' thisX x y {prfEq} = MkPair x y
2020-07-10 21:00:38 +01:00
Jan de Muijnck-Hughes
fcbfcf6fe2
Added take
to Vect.
2020-07-10 21:00:38 +01:00
Edwin Brady
9156084075
Merge pull request #449 from ohad/specifying-vector-transposition
...
Include a (non-linear) definition for transpose that uses zipWith
2020-07-10 18:09:27 +01:00
Denis Buzdalov
0aeadbad19
Recently added implementation were slightly fixed and nicened.
2020-07-10 17:28:49 +01:00
Ohad Kammar
eceaf98007
Generalise cons-specialised linear zipWith to linear zipWith (lzipWith)
2020-07-10 17:17:19 +01:00
Edwin Brady
606059e3d9
Merge pull request #451 from edwinb/impl-docs
...
Add some implementation notes to the docs
2020-07-10 16:25:26 +01:00
Edwin Brady
da4885c4fa
Fix formatting
2020-07-10 16:01:17 +01:00
Edwin Brady
874587906f
A few more internal details in the docs
2020-07-10 15:59:47 +01:00
Edwin Brady
3312961b54
Fix reference id
2020-07-10 15:23:44 +01:00
Edwin Brady
56e21fa27a
Add some implementation notes to the docs
2020-07-10 15:21:24 +01:00
Dmitry
c35b8e39f7
Add command line option to typecheck package without codegen ( #412 )
2020-07-10 14:08:21 +01:00
Ohad Kammar
8f09ef9b93
Include a (non-linear) definition for transpose that uses zipWith,
...
as it might be easier to reason about, since users may already have proved
stuff about zipWith that they want to reuse
2020-07-10 12:47:05 +01:00
Niklas Larsson
4a5ca77cbe
Make the idris2 executable depend on the idris2 lib
2020-07-10 12:46:44 +02:00
Niklas Larsson
ffb1d6406f
Merge pull request #445 from melted/update_ipkg
...
Update ipkg files
2020-07-10 11:28:20 +02:00
Niklas Larsson
a5b101dc3c
Update ipkg files
2020-07-10 11:03:21 +02:00
Niklas Larsson
80f4ced386
Merge pull request #442 from melted/fix_bootstrap2
...
Fix bootstrap
2020-07-10 00:48:26 +02:00
Niklas Larsson
cddf8c6fa5
Fix bootstrap
...
Replace if-expression with a function
2020-07-09 22:46:21 +02:00
Matthew Ess
6452cdbbd4
Add Ord
implementation for Either
( #439 )
2020-07-09 19:28:59 +01:00
SmiVan
3c051f3375
Amend typo in INSTALL.md
2020-07-09 11:58:53 +01:00
Niklas Larsson
eca9c12cf5
Merge pull request #438 from melted/fix_b
...
Fix bootstrap
2020-07-09 00:45:30 +02:00
Niklas Larsson
1d7378778a
Fix bootstrap
...
This was broken in #425 , because Idris2-boot hasn't implemented the
fix for #116
2020-07-09 00:04:03 +02:00
Niklas Larsson
b955d2e50c
Merge pull request #436 from edwinb/update-js
...
Update JS code generator to remove RF
2020-07-09 00:03:51 +02:00
Edwin Brady
2ab2adec0b
Update JS code generator to remove RF
...
This name was removed in a recent patch, leading to a small conflict.
Also added a note to the CHANGELOG and a placeholder in the docs.
2020-07-08 22:40:47 +01:00
Edwin Brady
23cbc28b1d
Merge pull request #415 from rbarreiro/javascript
...
Javascript
2020-07-08 22:27:58 +01:00
Edwin Brady
28b52fbc48
Merge pull request #432 from edwinb/docstrings
...
Initial implementation of :doc and :browse
2020-07-08 18:28:14 +01:00
Edwin Brady
2696130720
Update CHANGELOG for :doc and :browse
2020-07-08 18:06:02 +01:00
Edwin Brady
6dce3a0735
Add :browse
...
Lists all the names in a namespace with their types, and the first line
of their docstring if it exists
2020-07-08 17:56:54 +01:00
Edwin Brady
b0c226f05b
Extract interface info from hints
2020-07-08 17:21:28 +01:00
Edwin Brady
656a9d8f98
Also display methods of interfaces
...
Displaying implementations is a better harder at the moment, since
they're implemented via search hints...
2020-07-08 16:52:56 +01:00
Niklas Larsson
ae5398e41f
Merge pull request #431 from cypheon/lambdalift-new-casewith-names
...
Make sure names derived from case and with blocks get unique names during LambdaLifting
2020-07-08 17:13:32 +02:00
Edwin Brady
ff46a8db14
Initial implementation of :doc
...
It's not pretty, but at least it exists now
2020-07-08 15:52:57 +01:00
Guillaume ALLAIS
301666b91d
[ fix #423 ] --repl should load the main file
2020-07-08 15:29:37 +01:00
Guillaume ALLAIS
e277054fda
[ refactor ] lift partitionEithers to toplevel
2020-07-08 15:29:37 +01:00
Guillaume ALLAIS
b19a8e0a2c
[ cleanup ] trailing whitespace
2020-07-08 15:29:37 +01:00
Johann Rudloff
61987b89bd
Make sure names derived from case and with blocks get unique names during LambdaLifting
2020-07-08 16:22:15 +02:00
Niklas Larsson
21e95a95d8
Merge pull request #428 from melted/remove_ccall
...
Remove prim__cCall
2020-07-08 13:52:26 +02:00
Niklas Larsson
fc6b184106
Remove prim__cCall
...
It's not used anymore and %foreign is preferred.
2020-07-08 11:45:41 +02:00
Edwin Brady
2959829605
Merge pull request #426 from edwinb/record-implicits
...
Leave implicit record fields alone on update
2020-07-08 00:33:23 +01:00
Edwin Brady
58359c2d01
Leave implicit record fields alone on update
...
Unless an explicit update is given
2020-07-07 22:36:15 +01:00
Matus Tejiscak
634fe4d171
Fix tests.
2020-07-07 21:06:35 +01:00
Matus Tejiscak
168e5d8a21
Update postfix projection doc.
2020-07-07 21:06:35 +01:00
Matus Tejiscak
98e94f956e
Rename record projections to postfix projections.
2020-07-07 21:06:35 +01:00
Matus Tejiscak
4af4ae01ae
Update the postfix projection doc.
2020-07-07 21:06:35 +01:00