Denis Buzdalov
a7fb6722a0
[ re #2533 ] Fix recently added reflection's Show ( #2543 )
2022-06-16 11:08:51 +01:00
Denis Buzdalov
45579795bc
[ elab ] Make any error in elab script to produce a special error type
2022-06-16 09:49:56 +01:00
Denis Buzdalov
742d41f696
[ elab ] Make actual bad script errors be reported so
2022-06-16 09:49:56 +01:00
Denis Buzdalov
df6f4f69cd
[ doc ] Add clarification to the doc of a function of Elaboration
2022-06-16 09:49:56 +01:00
Denis Buzdalov
e590014fb7
[ cleanup ] Remove unused expression
2022-06-16 09:49:56 +01:00
G. Allais
bdf3833df5
[ new ] Auto in Agda (+ bonus) ( #2541 )
...
* [ new ] Auto in Agda (+ bonus)
* [ minor ] use DN for more readable terms
2022-06-16 09:35:45 +01:00
Guillaume Allais
cd324f9ff3
[ base ] Name convenience functions
2022-06-14 16:07:37 +01:00
Guillaume Allais
c9dbc3d743
[ new ] Show implementations for Language.Reflection
2022-06-14 16:07:37 +01:00
Guillaume Allais
381441d849
[ base ] maximum is an upper bound
2022-06-14 16:07:37 +01:00
Guillaume Allais
2060535d08
[ new ] name hints for primitive types
2022-06-14 16:07:37 +01:00
Guillaume Allais
a8fe4a778c
[ base ] Show for Constants
2022-06-14 16:07:37 +01:00
Guillaume Allais
128099fd47
[ debug ] better eval logging
2022-06-09 23:09:38 +01:00
Thomas E. Hansen
268a3520f3
[ base ] Port most of List.Quantifiers to List1
...
This doesn't include `Interleaving` and `Split`.
2022-06-09 09:05:10 +02:00
Thomas E. Hansen
5da3bc7d7c
[ base ] Port List.Elem to List1
2022-06-09 09:05:10 +02:00
Guillaume Allais
a6a4593aba
[ fuzzysearch ] don't print holes
2022-06-08 22:44:55 +01:00
Guillaume Allais
7bd7f1da9c
[ fix ] resugaring of DPair
2022-06-08 22:44:55 +01:00
Guillaume Allais
492abf7743
[ new ] better parse error for %language
2022-06-08 22:44:55 +01:00
György Kurucz
79a2f677d4
[ re #1282 ] Improve unelaboration of case expressions
2022-06-08 17:01:36 +01:00
Zoe Stafford
88c18621e6
Merge pull request #2529 from idris-lang/revert-2496-trans-deps
...
Revert "Transitive dependencies v2"
2022-06-08 07:49:58 +01:00
Zoe Stafford
b9001439b3
Revert "Transitive dependencies v2 ( #2496 )"
...
This reverts commit 51f952714d
2022-06-08 06:35:39 +01:00
Zoe Stafford
51f952714d
Transitive dependencies v2 ( #2496 )
...
* make `depends` collect all transitive dependencies
This happens by installing the (modified) ipkg file along with ttc files
* [ fix ] parsing a package shouldn't always set sourceDir
* linter *sigh*
* Fix test, add changelog
`asDepends` has been changed to `setSrc` as that is for me more intuitive
in idris2/pkg006 the version field was removed from the ipkgs of bar-baz and quux
as idris now expects the version to match the folder
idris2/pkg010 explicitly disables incremental compilation, to prevent extra log info
* (hopefully) fix idris2/pkg13 test on windows
* Actually install the version
This should make things start working
2022-06-07 14:31:14 +01:00
Steve Dunham
a197300f77
Include "showmachinenames" in the output of :opts
2022-06-06 07:51:02 +01:00
kasiaMarek
094a9ab06d
List proofs ( #2497 )
...
* Modified bind definition
* bind proofs and list elem proof
Co-authored-by: Katarzyna Marek <katarzynamarek@Katarzynas-MBP.lan>
2022-06-01 13:16:17 +01:00
G. Allais
d786b5d153
[ IDE ] auto completions ( #2511 )
2022-06-01 10:26:47 +01:00
fetsorn
af04b00270
fix typo in interactive.rst
2022-05-31 09:36:05 +01:00
G. Allais
5e9a90bd97
[ fix ] semantic highlighting in IDE mode ( #2509 )
...
* [ fix ] semantic highlighting in IDE mode
Bring back (?) highlighting of goals
* [ debug ] better logging: add length
* [ test ] turns out lengths are not needed!
2022-05-28 11:23:07 +01:00
G. Allais
071d37197a
[ IDE ] intro command ( #2502 )
2022-05-27 10:54:34 +01:00
Denis Buzdalov
599027a893
[ fix ] Make able to interpret result of a macro as a function
2022-05-27 09:36:44 +01:00
Denis Buzdalov
cb422443eb
[ refactor ] Simplify %runElab wrapping code of %macro
2022-05-27 09:36:44 +01:00
Denis Buzdalov
a766c628e9
[ base ] Add mapping functions to Data.Vect.Quantifiers
2022-05-27 09:03:28 +01:00
Xerz
e9f562f435
[ prelude ] Add Range implementation for Char ( #2505 )
2022-05-27 07:57:59 +01:00
Guillaume Allais
37c9c06f72
[ fix ] Actually send an answer back to IDE mode
2022-05-25 16:33:51 +01:00
G. Allais
607a2a2110
[ IDE ] refine command ( #2490 )
2022-05-25 11:29:03 +01:00
Zoe Stafford
9e92e7ded0
Merge pull request #2495 from idris-lang/revert-2469-trans-deps
...
Revert "make `depends` collect all transitive dependencies"
2022-05-21 07:32:47 +01:00
Zoe Stafford
932a24baa1
Revert "make depends collect all transitive dependencies ( #2469 )"
...
This reverts commit fde6269c7e
2022-05-21 06:49:07 +01:00
Zoe Stafford
fde6269c7e
make depends collect all transitive dependencies ( #2469 )
...
* make `depends` collect all transitive dependencies
This happens by installing the (modified) ipkg file along with ttc files
* [ fix ] parsing a package shouldn't always set sourceDir
* linter *sigh*
* Fix test, add changelog
`asDepends` has been changed to `setSrc` as that is for me more intuitive
in idris2/pkg006 the version field was removed from the ipkgs of bar-baz and quux
as idris now expects the version to match the folder
idris2/pkg010 explicitly disables incremental compilation, to prevent extra log info
* (hopefully) fix idris2/pkg13 test on windows
2022-05-20 16:20:54 +01:00
Denis Buzdalov
73608cb264
[ cleanup ] Clean up DecEq implementations with biinjective functions
2022-05-20 11:50:46 +01:00
Denis Buzdalov
d3fa76052b
[ new ] Introduce a Biinjective interface
2022-05-20 11:50:46 +01:00
Denis Buzdalov
a3542ad0cd
[ cleanup ] Make existing equality proofs a bit cleaner
2022-05-20 11:50:46 +01:00
Denis Buzdalov
4032ef2b85
[ base ] Implement equalities for inclusive-or type (These)
2022-05-19 13:37:28 +01:00
Nil Geisweiller
4ff5ff63a5
Escape \ in the code example of lambdaAbstraction doc
2022-05-19 11:57:31 +01:00
Nil Geisweiller
7461c3f538
Fix typo: Calculutor -> Calculator
2022-05-19 11:50:48 +01:00
Thomas Dziedzic
8bd5ca9492
[ doc ] cookbook for parsing ( #2484 )
2022-05-18 13:17:12 +01:00
Denis Buzdalov
95caed3c4f
[ refactor ] Support alternative equalities for TTImp
2022-05-18 11:12:05 +01:00
G. Allais
10a6734bcb
[ new ] Katla-powered landing page ( #2483 )
2022-05-18 08:43:47 +01:00
Guillaume Allais
7a863556c5
[ fix ] missing Show implementation
2022-05-17 16:50:50 +01:00
G. Allais
fdbd858d97
[ refactoring ] expose some internals needed by Katla ( #2480 )
2022-05-16 20:37:08 +01:00
Zoe Stafford
71351a6c88
Merge pull request #2476 from Z-snails/bits64-popcount
...
Fix `FiniteBits` for `Bits64`
2022-05-14 14:05:37 +01:00
Zoe Stafford
8a0d75dc6d
Fix FiniteBits for Bits64
2022-05-14 13:12:16 +01:00
Denis Buzdalov
72f0a2ab09
[ re #950 ] Remove redunant legacy data definition
...
`Given` with `Always` from Idris 1 library are completely overridden by
`IsYes` and `ItIsYes` respectively, which have a more common naming.
This, however, may break some very old code (fixed by a trivial rename).
2022-05-14 08:24:20 +01:00
