BlackBrane
afe9481871
Make clear that sum' is a synonym for concat
2015-08-03 14:02:34 +02:00
BlackBrane
44ca9c2d6a
Remove spurious Data.Fin imports (now reexported by Vect)
2015-08-02 19:49:43 +02:00
Edwin Brady
5a08c2cdb7
Proof search tweak
...
When checking types of hints, don't consider the recursive call as an
overlapping constructor type, or lots of things don't get filled in
which should be.
2015-08-02 14:36:06 +01:00
Edwin Brady
96e9b1a79e
Variable names in makelemma types
...
Put the variable names even if they aren't used, so that it's clearer
which is which at the definition site.
2015-08-02 14:36:06 +01:00
Niklas Larsson
a8f3171d56
Merge pull request #2494 from uwap/master
...
Make --mkdoc follow the sourcedir
2015-08-02 13:58:04 +02:00
uwap
61f02bfee1
Make --mkdoc follow the sourcedir
...
If you had an ipkg with a sourcedir defined before using the --mkdoc option would fail saying that some source files are missing.
This is because it didn't follow the sourcedir.
2015-08-02 02:50:57 +02:00
Edwin Brady
7095d6c1ed
Proof search should only use user visible names
...
If they are implicits or class arguments, it's fine for 'auto' to see
them since they're only used internally, but interactive proof search
will give odd results if it uses them. So, we make a list of names which
proof search in interactive mode is allowed to use.
2015-08-01 21:12:14 +01:00
Edwin Brady
8dd2a7f078
Make interactive proof search less enthusiastic
...
Instead of guessing, it will only fill in a metavariable if all of the
available constructors/hints have disjoint types. This means you'll no
longer always get 'Nothing' for Maybe or '[]' for List, but rather
you'll get a new metavariable.
'auto' behaves as before, because the idea there is to find any old
thing with the right type.
It feels like interactive proof search should be a bit more refined,
though, because the idea of that is to find the program you really want,
rather than any old program...
More refinements to this are likely, for example refusing to fill in
with locals if there are clashing types.
2015-08-01 15:57:30 +01:00
Edwin Brady
a4596d92b8
Tidy up 'tidy'(!)
...
Normalise the return type as well as th arguments.
2015-08-01 15:57:30 +01:00
Edwin Brady
0f80f562a0
Don't want newline after makeCase
2015-08-01 15:57:30 +01:00
Niklas Larsson
2c7563c4e3
Merge pull request #2492 from BlackBrane/master
...
Refinement & reorganization of Data.Matrix
2015-08-01 15:50:43 +02:00
BlackBrane
d649f2e228
Separate numeric/algebraic matrix ops from basic matrix functions
2015-07-31 17:56:08 +02:00
Niklas Larsson
546458e0d6
Merge pull request #2491 from ziman/ffi-fix
...
Make `FFI_Exportable` usable with other back-ends
2015-07-31 13:12:26 +02:00
Matus Tejiscak
098656e423
Make FFI_Exportable more generic.
2015-07-31 00:50:03 +01:00
Niklas Larsson
d05f550dc9
Merge pull request #2487 from uwap/patch-1
...
Fix documentation for distributivity of rings
2015-07-30 22:13:29 +02:00
Edwin Brady
5bd5777fb7
Add :makecase (:mc) to REPL and ide-mode
...
Replaces a metavariable with a case block, with an _ for the scrutinee
(much like :makewith)
I just got bored of typing these :). There is a corresponding update to
idris-vim.
2015-07-30 16:31:59 +01:00
Niklas Larsson
798958d464
Merge pull request #2486 from worldsayshi/patch-2
...
Fixed styling for multi line string literal docs
2015-07-30 02:42:07 +02:00
uwap
95fe866302
Fix documentation for distributivity of rings
...
Rings have a distributivity law between `<.>` and `<+>` not between `<.>` and `<->`
2015-07-30 02:35:59 +02:00
worldsayshi
b1ce657699
Fixed styling for multi line string literal docs
2015-07-30 00:31:17 +02:00
Niklas Larsson
bc4b4852e7
Merge pull request #2485 from worldsayshi/patch-1
...
Added docs on multiline strings
2015-07-30 00:26:58 +02:00
Niklas Larsson
7fe42e06de
Merge pull request #2470 from benjamin-hodgson/2460_multipleFields
...
Multiple record fields on one line (#2460 )
2015-07-30 00:26:43 +02:00
Benjamin Hodgson
f25976d7cb
Revert "Allow an optional trailing comma in commaSeparated"
...
The consensus following the discussion in the pull request
seemed to be by-and-large against allowing trailing commas.
So they're out.
This reverts commit 856d62dd84
2015-07-29 22:24:10 +01:00
worldsayshi
f5e56a6c96
typo when correcting typo
2015-07-29 18:19:51 +02:00
worldsayshi
b6fd66302e
added multi line strings doc and fixed typo
2015-07-29 18:12:21 +02:00
Niklas Larsson
af79c58c9c
Merge pull request #2484 from melted/ops
...
Sync the documentation with opChars in ParseHelpers.hs
2015-07-29 12:55:08 +02:00
Edwin Brady
ebf7a76305
Slightly less annoying name choice
...
x, y, z, x1, y1, ... instead of x, x1, x2, ... when no other hint for
names is given
2015-07-29 11:35:25 +01:00
Edwin Brady
b49c2fd6e3
Better display of classes in makeLemma
2015-07-29 11:27:37 +01:00
Niklas Larsson
a26562a666
Sync the documentation with opChars in ParseHelpers.hs
...
# and backslash was missing, and underscore isn't an operator char
2015-07-29 00:20:34 +02:00
Edwin Brady
1b96024f48
Add a couple of convenience functions in Data.Vect
...
I often want to do this sort of thing, perhaps others do too...
2015-07-28 21:43:02 +01:00
Edwin Brady
874ac98f40
Allow empty instance declarations in mutual blocks
...
This was supposed to work, but didn't, meaning that it was impossible to
use interactive tools to populate instance bodies in mutual blocks.
2015-07-28 18:17:44 +01:00
David Christiansen
e8b7737df1
Merge pull request #2482 from david-christiansen/issue/2481
...
Properly reify reflected character constants
2015-07-28 08:29:01 -06:00
David Raymond Christiansen
56869f69db
Properly reify reflected character constants
...
Fixes #2481
2015-07-28 06:59:35 -06:00
Edwin Brady
0e7c076058
Normalise types before detecting parametric args
...
Otherwise we miss some, and some annoying things fail as a result
(notably, trying to make aliases for type classes in functions)
2015-07-28 10:21:45 +01:00
Edwin Brady
80a2cee339
A few prelude functions/casts
2015-07-28 10:21:44 +01:00
Jan de Muijnck-Hughes
51bbaf91e8
Merge pull request #2480 from jeremy-w/jeremy-w/correct-mathsing-to-testing
...
Rewrite "mathsing" to "testing"
2015-07-28 09:38:57 +01:00
Jan de Muijnck-Hughes
c157e070a8
Merge pull request #2478 from jeremy-w/jeremy-w/updates-bst-module-reference-to-Btree
...
Update bst module reference to Btree
2015-07-28 09:38:32 +01:00
Jan de Muijnck-Hughes
21903a476a
Merge pull request #2477 from jeremy-w/jeremy-w/removes-early-splitAt
...
Remove |splitAt| from let-binding section
2015-07-28 09:37:50 +01:00
Jeremy W. Sherman
d03e2b018a
Rewrite "mathsing" to "testing"
...
Looks like global search and replace changed "test" -> "maths" at some point.
2015-07-28 00:29:47 -04:00
Jeremy W. Sherman
0b8f521a84
Capitalize module name to match code sample
...
|btree| -> |Btree|
2015-07-28 00:06:09 -04:00
Jeremy W. Sherman
3ad394ec27
Update module name to |Btree| to match code sample
...
The code sample shows the module named |Btree| now.
|bst| was perhaps carried over from an older revision?
2015-07-27 23:59:00 -04:00
Jeremy W. Sherman
61fcd57244
Remove |splitAt| from let-binding section
...
|splitAt| is still introduced and discussed in the case expressions section.
Its appearance in the let-binding section looks like an accident.
2015-07-27 23:34:05 -04:00
Niklas Larsson
5339208f04
Merge pull request #2476 from athanclark/patch-1
...
Fixing typo
2015-07-28 02:39:03 +02:00
Athan Clark
7fca841b31
Fixing typo
2015-07-27 17:49:11 -06:00
Niklas Larsson
b89ea52685
Merge pull request #2473 from xged/unlines
...
Add functions `unlines`, `unlines'` to Prelude.String
2015-07-27 16:54:26 +02:00
xged
b659ab8cdb
Add functions , to Prelude.String
2015-07-27 15:48:47 +03:00
Benjamin Hodgson
856d62dd84
Allow an optional trailing comma in commaSeparated
2015-07-26 19:06:10 +01:00
Benjamin Hodgson
9a9b797ce6
Add documentation for #2460
2015-07-26 16:45:55 +01:00
Benjamin Hodgson
f1e8a4dcc9
Multiple record fields on one line ( #2460 )
...
You can now write this:
```
record Person where
constructor MkPerson
name, surname, middleName : String
```
- which is equivalent to:
```
record Person where
constructor MkPerson
name : String
surname : String
middleName : String
```
I changed the parser a little and added a test for the new functionality.
2015-07-26 16:29:26 +01:00
Niklas Larsson
ffb7946730
Merge pull request #2469 from lenary/add-stack
...
Add Stackage Configuration for easy building
2015-07-25 21:45:58 +02:00
Niklas Larsson
54e4e41b49
Merge pull request #2468 from benjamin-hodgson/patch-1
...
Fix Multiplicative/Additive docs
2015-07-25 21:44:29 +02:00
