idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-24 20:23:11 +03:00
Code Issues Projects Releases Wiki Activity
3,701 Commits 6 Branches 9 Tags 115 MiB
ce2790d6f9
Commit Graph

3701 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Justus Matthiesen
873b3edd29
[ fix #3143 ] traverse as-patterns when constructing terms matching an impossible LHS (#3146) 
* [ fix #3143 ] traverse as-patterns in `getImpossibleTerm`

* [ test ] impossible as-pattern
 2023-11-23 08:29:15 +00:00
Justus Matthiesen
154dcec76f [ cleanup ] heterogeneous eqTerm makes believe_me unnecessary 2023-11-23 08:28:38 +00:00
Guillaume Allais
ba973531f7 [ cleanup ] remove dead code MkSeqConstraint 2023-11-23 08:27:35 +00:00
Steve Dunham
a03c3bf376 [ doc ] Add missing pragmas to documentation 2023-11-22 09:13:42 -08:00
André Videla
d6aa70dbe1
Merge pull request #2669 from joelberkeley/documentation 
refactor README and installation instructions
 2023-11-15 00:35:46 +00:00
Joel Berkeley
54c83cd80b
wording 
Co-authored-by: CodingCellist <teh6@st-andrews.ac.uk>
 2023-11-13 11:42:27 +00:00
Steve Dunham
af10fbaf94 [ error ] Improve parse errors in ipkg files 2023-11-12 10:09:50 +00:00
Joel Berkeley
2520f4eb7b line length 2023-11-11 16:11:02 +00:00
Joel Berkeley
a0887401a6 line length 2023-11-11 16:10:13 +00:00
Joel Berkeley
d7d97d45ad line length 2023-11-11 16:09:23 +00:00
Joel Berkeley
323f1d0186 line length 2023-11-11 16:02:33 +00:00
Joel Berkeley
a409f11d39 wording 2023-11-11 15:57:02 +00:00
Joel Berkeley
fec32e45f8 wording 2023-11-11 15:55:19 +00:00
Joel Berkeley
9608086669 link map of source code 2023-11-11 15:54:09 +00:00
Joel Berkeley
1e7aee47d8 typo 2023-11-11 02:11:50 +00:00
Joel Berkeley
92d36fb19c link videos and map of source code 2023-11-11 02:10:17 +00:00
Joel Berkeley
978f956012 remove icon 2023-11-10 13:38:12 +00:00
Joel Berkeley
9b4c4d8efd icon attempt 5 2023-11-10 13:35:57 +00:00
Joel Berkeley
54eec37572 icon attempt 4 2023-11-10 13:35:24 +00:00
Joel Berkeley
0795d9cb00 icon attempt 3 2023-11-10 13:34:57 +00:00
Joel Berkeley
4c5bfbc95c icon attempt 2 2023-11-10 13:31:54 +00:00
Joel Berkeley
6abffe22d0 icon first attempt 2023-11-10 13:28:37 +00:00
Joel Berkeley
e66b79fc2c mention Node version requirement 2023-11-10 13:09:27 +00:00
Joel Berkeley
3f1784a163 simplify TOC in INSTALL 2023-11-10 13:07:07 +00:00
Joel Berkeley
e048896179 Install -> Installing 2023-11-10 12:59:19 +00:00
Joel Berkeley
6a6ad983db pack link points to homepage 2023-11-09 23:33:29 +00:00
Joel Berkeley
b26bd7d4b4 remove pack installation instructions 2023-11-09 23:16:54 +00:00
Joel Berkeley
4d0410a7d3 alternative links 2023-11-09 23:13:07 +00:00
Joel Berkeley
c4b3069a6f refactor README and installation instructions 2023-11-09 22:58:02 +00:00
Denis Buzdalov
1aff26e94c [ test ] Reduce the need of frequent golden vals updates in one test 2023-11-09 22:05:36 +00:00
Denis Buzdalov
2c328a51c0 [ elab ] Support more applicative traversals of TTImp 2023-11-09 22:05:36 +00:00
CodingCellist
d80bc1537d
[ base ] Add bindings for ieee Double number consts (#3116) 2023-11-09 14:01:40 +00:00
Steve Dunham
a945b5d2df [ ffi ] Fix missing structure declarations in scheme ffi 2023-11-09 14:00:20 +00:00
Justus Matthiesen
db4c5e7fbb
Cleanup of sizeEq (#3138) 2023-11-09 13:59:53 +00:00
PHO
7c87005092
Support "make -j" (#3135) 
* Allow Idris2 to bootstrap with "make -j"

"linear" should explicitly depend on "base" so that "base" is built before
"linear", otherwise it can fail with:

> Error: Module Data.Nat not found
>
> Data.Linear.Copies:5:1--5:16
>  1 | module Data.Linear.Copies
>  2 |
>  3 | import Data.Linear.Bifunctor
>  4 | import Data.Linear.Notation
>  5 | import Data.Nat
>      ^^^^^^^^^^^^^^^

* Allow Idris2 to build with "make -j all"

"all: ${TARGET} libs" is bad because it means "${TARGET}" and "libs" can be
built independently. So "make -j" attempts to build them parallelly and
fail.
 2023-11-08 08:18:02 +00:00
Justus Matthiesen
a26766e57a [ doc ] bring findLoops and checkNonDesc description back in sync 2023-11-06 20:10:21 +00:00
Justus Matthiesen
8e34332c08 [ cleanup ] remove unneeded debug messages 2023-11-06 20:10:21 +00:00
Justus Matthiesen
a84ba3b1ef [ doc ] bring description of mkChange back in sync 2023-11-06 20:10:21 +00:00
Justus Matthiesen
bc386dab4e [ cleanup ] bring formatting of sc-graphs in tests back in sync 2023-11-06 20:10:21 +00:00
Justus Matthiesen
ba19fae07a [ fix ] handle printing of empty matrices gracefully 2023-11-06 20:10:21 +00:00
Justus Matthiesen
39f3aeeb08 [ cleanup ] remove 1 suffix from Vector1 functions 2023-11-06 20:10:21 +00:00
Justus Matthiesen
291d60da08 [ cleanup ] move auxiliary function to where block 2023-11-06 20:10:21 +00:00
Justus Matthiesen
03484f2dfa [ cleanup ] split Vector and Vector1 into separate namespaces 2023-11-06 20:10:21 +00:00
Justus Matthiesen
c36be9291d [ doc ] clarification on neutrals 2023-11-06 20:10:21 +00:00
Justus Matthiesen
c36625d1db [ cleanup ] remove duplicate and unused functions 2023-11-06 20:10:21 +00:00
Justus Matthiesen
d9cc448d3e [ debug ] sc-graphs now have labels "l" and "r" for LHS and RHS 2023-11-06 20:10:21 +00:00
Justus Matthiesen
8c7c59a5d0 [ new ] labels for pretty-printed sparse matrices 2023-11-06 20:10:21 +00:00
Justus Matthiesen
8822040f37 [ new ] replicateChar, an analogue to spaces but for arbitrary Chars 2023-11-06 20:10:21 +00:00
Justus Matthiesen
80657feb34 [ doc ] sparse matrix invariants 2023-11-06 20:10:21 +00:00
Justus Matthiesen
e5788a3e86 [ test ] tracking size-change across applications 2023-11-06 20:10:21 +00:00