idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-24 15:07:37 +03:00
Code Issues Projects Releases Wiki Activity
894 Commits 5 Branches 9 Tags 96 MiB
62a5406533
Commit Graph

894 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Guillaume ALLAIS
62a5406533 [ fix #454 ] compiling nonexisting file 2020-07-14 15:23:00 +01:00
Mark Barbone
acda3b44a9
Make Text.Parser.between lazy (#385) 2020-07-14 14:33:22 +01:00
Dmitry
de00ff74d5
Allow to override log level with package options (#411) 2020-07-14 12:17:03 +01:00
G. Allais
0908e76515
[ fix #346 ] Pull List.length into prelude (#450) 2020-07-14 12:15:57 +01:00
Nicolas Biri
aba76206c9 Remove dependency to Vector length in deleteAt 2020-07-14 09:45:33 +01:00
Niklas Larsson
7920eb8a0e
Merge pull request #456 from chrrasmussen/patch-1 
Update reference to %auto_implicits in implementation notes
 2020-07-13 11:53:01 +02:00
Niklas Larsson
26f9c8a25c
Merge pull request #459 from rbarreiro/master 
fix #447
 2020-07-13 10:18:36 +02:00
Niklas Larsson
d6c4393517
Merge pull request #427 from nickdrozd/more-changes 
Minor simplifications
 2020-07-13 10:17:31 +02:00
Nick Drozd
e14a589e90 Consolidate boolean expressions 2020-07-12 21:00:33 -05:00
Nick Drozd
6519b5608d Further simplify List 2020-07-12 21:00:33 -05:00
Nick Drozd
718da3d7e6 Simplify Vect 2020-07-12 20:59:00 -05:00
Edwin Brady
e93fba3952
Merge pull request #462 from edwinb/prelude-org 
Reorganising the prelude
 2020-07-13 01:30:01 +01:00
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
Rui Barreiro
bfecdb41d1 trigger ci 2020-07-12 11:59:58 +01:00
Rui Barreiro
98f2b8a246 update test 2020-07-12 10:26:30 +01:00
Rui Barreiro
ccf441f42b fix #447 2020-07-12 10:13:45 +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
Christian Rasmussen
6211922960
%auto_implicit has been renamed to %unbound_implicits 2020-07-11 02:33:23 +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