Matus Tejiscak
f478a03b69
Allow arbitrary expressions in postfix projections.
2020-07-07 21:06:35 +01:00
Matus Tejiscak
3b6d7a22e3
Remove forgotten .field from docs.
2020-07-07 21:06:35 +01:00
Matus Tejiscak
b46064f688
Update docs and tests.
2020-07-07 21:06:35 +01:00
Matus Tejiscak
3484510f5a
Implement postfix dotted application.
2020-07-07 21:06:35 +01:00
Niklas Larsson
c4608745f7
Merge pull request #424 from markuspf/remove-superflous-argument
...
Remove a superflousy declared argument to idris2_openFile
2020-07-07 13:37:36 +02:00
Markus Pfeiffer
63ddd149ed
Remove a superflousy declared argument to idris2_openFile
...
This didn't cause a problem before as it was likely just ignored by the C
function. According to Edwin the extra argument is a leftover from when this
was a pure scheme call.
2020-07-07 11:44:37 +01:00
arty
1d14026f9d
Add comment about TTC files in TTC error
2020-07-07 11:20:04 +01:00
Nick Drozd
7d5788471d
Update tests
2020-07-07 10:48:23 +01:00
Nick Drozd
2ae6e06565
Simplify Fin
2020-07-07 10:48:23 +01:00
Nick Drozd
7d1ee9dd08
Simplify Equality
2020-07-07 10:48:23 +01:00
Nick Drozd
48fe4382eb
Simplify List
2020-07-07 10:48:23 +01:00
Nick Drozd
877f3702ad
Simplify Maybe
2020-07-07 10:48:23 +01:00
Nick Drozd
465be9cb86
Simplify Either
2020-07-07 10:48:23 +01:00
Nick Drozd
faabbfcea1
Add some Uninhabited implementations
2020-07-07 10:48:23 +01:00
Nick Drozd
7c923944ae
Add %default total to a few modules
2020-07-07 10:48:23 +01:00
Michael Birch
5c9339bde8
Merge sort implementation for Vect ( #417 )
2020-07-07 10:25:42 +01:00
Edwin Brady
77ad6eac0a
Merge pull request #422 from edwinb/record-implicits
...
Pay attention to implicits in record update
2020-07-06 18:06:43 +01:00
Edwin Brady
0cf37f621b
Pay attention to implicits in record update
...
Resolves #421
2020-07-06 17:39:55 +01:00
Niklas Larsson
468c8cbae3
Merge pull request #414 from melted/simple_parser
...
Add a simple parser combinator library for strings
2020-07-06 17:16:19 +02:00
Edwin Brady
50435cc1a1
Merge pull request #420 from edwinb/some-fixes
...
Resolving some issues
2020-07-06 15:17:21 +01:00
Edwin Brady
f649a61f4d
More accurate comment!
...
The desugaring of alternatives will correspond, but the variable matches
won't necessarily.
2020-07-06 14:45:36 +01:00
Niklas Larsson
d9e9298eb3
Merge pull request #419 from markuspf/fix-closeDir-name
...
Fix forward declaration of idris_closeDir
2020-07-06 15:36:23 +02:00
Edwin Brady
abdadead0a
More liberal with alternatives in with blocks
...
Only need to match one possibility (it's essentially impossible to match
more than one after all!). Fixes #297 .
2020-07-06 14:23:15 +01:00
Edwin Brady
666ecb36b5
Preserve @ patterns when totality checking case
...
Resolves #300
2020-07-06 14:03:34 +01:00
Edwin Brady
e25f0a57f9
Use correct implicit generation function
...
Should make a default implicit, not an auto implicit, when running out
of arguments and expecting a default implicit. Fixes #371
2020-07-06 14:02:45 +01:00
Markus Pfeiffer
0b32bf8a2f
Fix forward declaration of idris_closeDir
2020-07-06 13:56:36 +01:00
Niklas Larsson
52c6db09d1
Add <?> for replacing error messages
2020-07-06 14:13:56 +02:00
Niklas Larsson
60a067fab1
Remove dumpState
2020-07-06 13:57:13 +02:00
Tim Engler
14725dac67
Describe what is meant by "use"
...
I hit a roadblock trying to understand linear types, because I couldn't figure out what is meant to "use" a variable. I eventually think I figured it out, by reading "Linear types can change the world!", but it was not easy to do so. I think a better description of what "use" means would be very helpful for those unfamiliar with linear types, so I took a stab at it. Hope it helps.
2020-07-06 12:38:03 +01:00
Denis Buzdalov
066b37feb4
Tiny doc fix about combination of import public and import .. as.
2020-07-06 11:23:56 +01:00
Niklas Larsson
5060eaafaf
Make things public export to work with bootstrap
2020-07-05 21:51:12 +02:00
Niklas Larsson
af83c9303b
Add test and documentation
2020-07-05 21:51:12 +02:00
Niklas Larsson
d779c85df4
Add optional
2020-07-05 21:51:11 +02:00
Niklas Larsson
0e51124a43
Add option
2020-07-05 21:51:11 +02:00
Niklas Larsson
bba15974a5
Add takeWhile
...
add substring and length primitives to Data.Strings
2020-07-05 21:51:11 +02:00
Niklas Larsson
a78ee1dfca
Expand test code a bit with pure parsing
2020-07-05 21:51:11 +02:00
Niklas Larsson
39535bf11a
Add lifting
2020-07-05 21:51:11 +02:00
Niklas Larsson
d97789190d
Add bounds checking
2020-07-05 21:51:11 +02:00
Niklas Larsson
f290c6c3ce
Start on a simple string parser
2020-07-05 21:51:11 +02:00
Edwin Brady
6f8aed5478
Merge pull request #416 from edwinb/with-name
...
Use a String, not an Int, for case/with names
2020-07-05 20:26:32 +01:00
Edwin Brady
8774df8800
Use a String, not an Int, for case/with names
...
The Int represented the resolved name, but this isn't guaranteed to be
up to date after reloading and, worse, it doesn't display helpfully. I'm
bored of updating the tests which fail as a result!
This also fixes #407 , which is about displaying the wrong name after
reloading the ttc.
2020-07-05 20:02:50 +01:00
Edwin Brady
7a0b25f994
Merge pull request #369 from cypheon/tailrec-unpack
...
Make Prelude.unpack tail-recursive
2020-07-05 14:11:02 +01:00
Edwin Brady
a9478875b3
Merge pull request #392 from buzden/append-properties
...
Injectivity and similar properties were added for lists'a append
2020-07-05 14:08:07 +01:00
Edwin Brady
e3dcc2da1b
Merge pull request #354 from stepancheg/generated
...
Insert @generated marker into generated Scheme files
2020-07-05 14:05:22 +01:00
Edwin Brady
5487290499
Merge pull request #282 from ether42/master
...
Fix MkRecord signature
2020-07-05 14:03:57 +01:00
Edwin Brady
9d1bb82c48
Merge pull request #242 from nickdrozd/algebra
...
Add Algebra interfaces and laws
2020-07-05 00:04:13 +01:00
Edwin Brady
2321513b86
Merge pull request #410 from edwinb/import-revise
...
A variety of namespace and import goodies
2020-07-05 00:02:36 +01:00
Edwin Brady
4c5d26f050
Add note on import...as to tutorial
2020-07-04 23:30:13 +01:00
Edwin Brady
6bb6ced43a
Remove name visibility check
...
It doesn't seem to serve any useful purpose, other than to annoy!
2020-07-04 23:12:15 +01:00
Edwin Brady
950431a9ce
Note in tutorial on qualified do
2020-07-04 23:12:03 +01:00
