idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-28 19:13:02 +03:00
Code Issues Projects Releases Wiki Activity
1,424 Commits 5 Branches 9 Tags 99 MiB
2eb8f4149c
Commit Graph

1424 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Stiopa Koltsov
2eb8f4149c idris2 --help now prints env variables used by the compiler 
Until yesterday I did not know Idris2 accesses environment variables.
Mentioning them in `--help` would educate other users.

Not all descriptions make sense, I tried my best to guess them.

Output is: [link](https://gist.github.com/stepancheg/7d1dff344a0dd35b9d07fb4a417ecb32).
 2021-01-18 10:40:47 +00:00
Stiopa Koltsov
7264d40c56 Make isElem, DecEq public, not just export 
... so they could be used in proof search.

Follow-up to #942
 2021-01-18 10:37:57 +00:00
Edwin Brady
9c54d659fe
Merge pull request #937 from edwinb/fix-tests 
Update test output
 2021-01-16 18:29:03 +00:00
Edwin Brady
c7783c553c Make the linter happier 2021-01-16 17:18:38 +00:00
Edwin Brady
60c6f0dd97 Merge github.com:idris-lang/Idris2 into fix-tests 2021-01-16 17:15:27 +00:00
Edwin Brady
9f906bed81 Update test output 
This was changed due to the recent multiplicity update.
 2021-01-16 17:09:02 +00:00
Edwin Brady
efae2682bd
Merge pull request #896 from Russoul/toString-iterators 
Add withIteratorString
 2021-01-16 15:47:45 +00:00
Edwin Brady
6df2955a72
Merge pull request #909 from stefan-hoeck/maybeT 
added MaybeT monad transformer to base
 2021-01-16 15:43:14 +00:00
Edwin Brady
70c87e49da
Merge pull request #920 from stefan-hoeck/eithert-foldable-fix 
fixed bug in Foldable of EitherT
 2021-01-16 15:40:33 +00:00
Guillaume Allais
fb77a3e043 [ lint ] remove trailing whitespace 2021-01-16 14:26:55 +00:00
Edwin Brady
25def217fb
Merge pull request #936 from edwinb/changelog 
Update CHANGELOG/CONTRIBUTORS
 2021-01-16 14:21:26 +00:00
Edwin Brady
ce1e43e15c Alphabetic order in CONTRIBUTORS 
vim's :sort is apparently case sensitive by default!
 2021-01-16 14:20:25 +00:00
Alex Gryzlov
c67fc5d7c0
add Inspect idiom (#919) 2021-01-16 14:18:34 +00:00
Edwin Brady
e1ecefa205 Update CHANGELOG/CONTRIBUTORS 
We need to keep the CONTRIBUTORS file up to date, to give people proper
credit where it's due. There may still be people missing - please feel
free to add your own name if you think it should be there!
 2021-01-16 14:18:18 +00:00
Edwin Brady
fec03ea598
Merge pull request #902 from mattpolzin/scratch-work-search-repl 
Interactive & REPL :search feature
 2021-01-16 14:11:41 +00:00
Edwin Brady
d492b6341b
Merge pull request #917 from jmd28/benchmark 
Benchmark Suite
 2021-01-16 14:08:32 +00:00
Edwin Brady
96257f23c3
Merge pull request #914 from stefan-hoeck/lazy-list-impls 
Eq, Ord, and Show instances for LazyList
 2021-01-16 14:07:26 +00:00
Stiopa Koltsov
54fd2bca4c Add .editorconfig 
Add .editorconfig to the repository to trim trailing whitespaces
and insert trailing newlines in many editors.

See also #931
 2021-01-16 10:02:14 +00:00
Stiopa Koltsov
b214cd58bd Print warning make test does not invoke make 
Took some time for me to figure that out.
 2021-01-16 10:00:46 +00:00
Stiopa Koltsov
6d89899a06 GitHub workflow to schedule linter 2021-01-16 10:00:03 +00:00
Stiopa Koltsov
b76c9d91e0 Remove trailing whitespaces and add trailing newlines 2021-01-16 10:00:03 +00:00
Stiopa Koltsov
423fdad135 Lint utility 
Validate .idr files have no trailing whitespaces or trailing newlines
 2021-01-16 10:00:03 +00:00
Fabián Heredia Montiel
d712ea288a Implement Racket Futures Support 2021-01-15 18:58:51 +00:00
Denis Buzdalov
4f05d227a6 List-level quantifier conversion to element-level and vice-versa 2021-01-15 18:57:01 +00:00
Denis Buzdalov
bcc8da5a6d Currying and uncurrying functions for dependent pairs were added. 2021-01-15 18:53:40 +00:00
GustavoMF31
fea21d88c5
Apply small refactors all around (#898) 2021-01-15 18:52:29 +00:00
Fabián Heredia Montiel
a15325fdb6
Update previous-build action from 0.2.2 to 0.3.0 (#925) 2021-01-15 18:00:46 +00:00
Guilherme Silva
7a7504c956
Added nix files (#855) 2021-01-15 17:20:52 +00:00
Denis Buzdalov
6d2dd935c4
Special variants of DPair as records (#922) 2021-01-15 17:19:20 +00:00
André Videla
bea840418a
Merge pull request #823 from andylokandy/path 
Changes to System.Path

- Rename `startWith` to `isBaseOf`
- Rename `stripPrefix` to `dropBase`
- Add `dropExtension`
- Add `splitPath`
 2021-01-14 22:09:04 +00:00
Andy Lok
4f8bd22b35 Use present tense in doc for Path 2021-01-14 05:26:42 +08:00
Andy Lok
f1d6d4d6f4 Use dot syntax to avoid path argument 2021-01-14 05:05:59 +08:00
Edwin Brady
8cee404736
Merge pull request #923 from edwinb/faq-update 
FAQ addition
 2021-01-13 16:31:58 +00:00
Edwin Brady
79a89a046f FAQ addition 2021-01-13 16:31:20 +00:00
Edwin Brady
bd94dbdd8e
Merge pull request #921 from edwinb/version030 
Update version numbers and bootstrap code
 2021-01-13 15:01:30 +00:00
Edwin Brady
e9f82afc4d CHANGELOG edits 2021-01-13 13:04:08 +00:00
Edwin Brady
b35268b774 Update version numbers and bootstrap code 2021-01-13 12:46:06 +00:00
stefan-hoeck
7b73072554 fixed bug in Foldable of EitherT 2021-01-13 13:21:20 +01:00
Stefan Hoeck
77a911aa8a
Update libs/base/Control/Monad/Maybe.idr 
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
 2021-01-13 11:19:03 +01:00
stefan-hoeck
e52b658d78 no linearity annotation for MkMaybeT 2021-01-13 05:34:07 +01:00
stefan-hoeck
2301826a4e improved documentation for 'on' 2021-01-13 05:06:01 +01:00
jmd28
807725f26d
Update readme.md 2021-01-12 13:33:57 +00:00
james
9f94198380 add benchmark suite 2021-01-12 13:22:58 +00:00
james
0ce0f5a8e7 add benchmark suite 2021-01-12 13:20:42 +00:00
Edwin Brady
3621c5d1bd
Merge pull request #879 from edwinb/no-linearity-subtyping 
Remove linearity subtyping
 2021-01-12 12:33:26 +00:00
Edwin Brady
fe602caa2c
Merge pull request #765 from ShinKage/ide-mode 
IDEMode syntax option and fixed output
 2021-01-12 10:39:44 +00:00
Edwin Brady
d4abbfdae2 Add HasLinearIO 
Ideally, liftIO would always be linear, but that has lots of knock-on
effects for other monads which we might want to put in HasIO, now that
subtyping is gone. We'll have to revisit this when we have some kind of
multiplicity polymorphism.
 2021-01-11 11:24:43 +00:00
stefan-hoeck
530e62a156 Eq, Ord, and Show instances for LazyList 2021-01-11 11:45:56 +01:00
stefan-hoeck
c39df89f84 deleted 'head' from Data.Stream 2021-01-11 09:36:13 +00:00
stefan-hoeck
31f50a793c added prelude function 'on' 2021-01-11 05:26:17 +01:00