David Christiansen
6fc713d2a9
Merge pull request #2606 from NightRa/patch-1
...
Fix a typo in the Cast documentation
2015-09-12 09:19:45 +02:00
David Christiansen
d583ff0ef8
Merge pull request #2607 from sdroege/faq-typo
...
faq: Fix typo in argument name of ifThenElse
2015-09-12 09:19:21 +02:00
Sebastian Dröge
f121da7417
faq: Fix typo in argument name of ifThenElse
2015-09-11 23:59:24 +02:00
Ilan Godik
053ffdce08
Fix a typo in the Cast documentation
2015-09-11 22:10:39 +03:00
Niklas Larsson
be157aabd7
Merge pull request #2604 from melted/clean_compile
...
Remove the --yes-really flag from codegens
2015-09-11 19:09:04 +02:00
Niklas Larsson
b19d03cfb9
Remove --yes-really
...
See discussion on #2579
2015-09-11 17:59:27 +02:00
Niklas Larsson
cb11c39a1c
Cleanup in Compiler.hs
2015-09-11 15:50:12 +02:00
Melvar Chen
319d143697
Remove obsolete reflected tactic
...
The search tactic and thus auto will do the same thing.
2015-09-11 14:56:30 +02:00
Melvar Chen
6e49c84c5e
Add Ordering composition and use it for Ord (Vect n a)
2015-09-11 14:56:30 +02:00
Melvar Chen
6b4c4d27b7
Give Vect.findIndices & Co a more useful type
2015-09-11 14:56:30 +02:00
Melvar Chen
3f24fac101
Clean up various Data.Vect functions
2015-09-11 14:56:30 +02:00
Melvar Chen
50b5031405
Merge VectType into Vect to be more like other Data.*
2015-09-11 14:56:30 +02:00
David Raymond Christiansen
bba27b6ba2
Remove +, -, and * on Fin
...
There are a number of reasonable type signatures for these, and there
doesn't seem to be a reason to prioritize the particular versions in the
library. They generated more questions than actual use.
2015-09-10 18:20:30 +02:00
David Raymond Christiansen
6cf7f5a9c5
Fix proof script deprecation warnings
2015-09-10 18:01:36 +02:00
David Raymond Christiansen
90bbf061dc
Add deprecation warning for %elim
...
The command-line option --no-elim-deprecation-warnings turns it off, so
that users wanting to write backwards-compatible libraries can still run
it.
2015-09-10 18:00:42 +02:00
David Christiansen
fa6a50ad5e
Merge pull request #2599 from scshunt/master
...
Use uninhabited instance for nonempty.
2015-09-10 17:32:20 +02:00
Sean Hunt
b9e9c52803
Add myself to CONTRIBUTORS.
2015-09-10 09:25:39 -04:00
Sean Hunt
8501e6d93b
Use uninhabited instance for nonempty.
2015-09-10 09:18:04 -04:00
David Raymond Christiansen
b28fecf6d2
Fix docstring
2015-09-10 14:14:57 +02:00
David Raymond Christiansen
752a2fcc77
Update tests for proof deprecation
2015-09-10 12:01:39 +02:00
David Raymond Christiansen
f4bcbbcd2f
Update CHANGELOG for deprecated tactics
2015-09-10 08:26:27 +02:00
David Raymond Christiansen
dfb42d1be9
Emit deprecation warning for old-style tactic proofs
2015-09-10 08:24:36 +02:00
David Raymond Christiansen
81a9095112
Add deprecation warning to old interactive prover
2015-09-10 08:24:25 +02:00
David Raymond Christiansen
f88a37794e
Add elaborator reflection to default namespace
2015-09-09 22:55:16 +02:00
David Raymond Christiansen
e947d69d74
Add conversion checking to Elab
2015-09-09 22:53:04 +02:00
David Christiansen
70d197efd4
Merge pull request #2595 from Melvar/fix-tests
...
Make test totality010 work when ncurses is enabled
2015-09-09 08:22:53 +02:00
David Christiansen
0600e99ee9
Merge pull request #2596 from Melvar/fix-chr
...
Make chr check for the correct range
2015-09-09 08:22:21 +02:00
David Christiansen
1f8944f6da
Merge pull request #2594 from david-christiansen/various-updates
...
Updates and fixes
2015-09-09 06:54:41 +02:00
Melvar Chen
52dd3090ed
Make chr check for the correct range
2015-09-09 03:29:15 +02:00
Melvar Chen
d846ce79de
Make test totality010 work when ncurses is enabled
2015-09-09 01:51:49 +02:00
David Raymond Christiansen
1cdc9ddfdc
Reduce space leak through ugly DeepSeq hack
...
The space leak documented in issue #2386 is helped by forcing the state
in a few places. Now, with the empty module, no space leak occurs, while
it grows by about 1 MB per 200 reloads with a large module. While
deepseqing the state is a hack, and should be better, I've not yet
improved on this and it does make Idris usable for repeated reloads of
large modules when using the interactive editing features.
2015-09-08 20:13:52 +02:00
Niklas Larsson
c6acf7fe31
Merge pull request #2593 from melted/issue-2568
...
Add exe to windows executables without extension when cleaning.
2015-09-08 02:56:05 +02:00
Niklas Larsson
98eb1af0b6
Add exe to windows executables without extension when cleaning.
...
So if it already has .exe, .js or something else it will not
be added.
Fixes #2568
2015-09-08 02:03:12 +02:00
Niklas Larsson
73c6bb4e96
Merge pull request #2592 from melted/bit-pattern
...
Allow pattern matching on BitX constants
2015-09-07 23:54:40 +02:00
Niklas Larsson
8564250334
Allow pattern matching on BitX constants
2015-09-07 21:59:26 +02:00
David Raymond Christiansen
6d426003ae
Show types in IDE namespace browser
2015-09-07 16:11:31 +02:00
David Raymond Christiansen
60b43b48b7
Add raw name quotes
...
The raw quote of name n, written `{{n}}, quotes n directly to its AST
without performing any lookup or resolution, allowing a much shorter
syntax.
2015-09-07 14:08:16 +02:00
David Raymond Christiansen
d952c941d4
Improve error message when reifying non-constant
...
Fixes #2521 .
2015-09-07 13:47:28 +02:00
David Raymond Christiansen
8902caca6f
Save context changes in interactive elab
...
Fixes #2544 .
2015-09-07 13:28:45 +02:00
Edwin Brady
f08e412b50
Merge branch 'master' of github.com:idris-lang/Idris-dev
2015-09-06 19:06:55 +01:00
Edwin Brady
eb38173a24
Merge branch 'jfdm-effLogging-updates'
2015-09-06 19:06:36 +01:00
Edwin Brady
c10d5700bd
Merge branch 'effLogging-updates' of https://github.com/jfdm/Idris-dev into jfdm-effLogging-updates
...
Conflicts:
CHANGELOG
2015-09-06 18:55:01 +01:00
Niklas Larsson
a0d8376256
Merge pull request #2518 from jeremy-w/jeremy-w/mark-interactive-proving-as-deprecated
...
Document interactive theorem proving as deprecated.
2015-09-06 19:43:53 +02:00
Niklas Larsson
88005d8619
Merge pull request #2572 from enolan/cabal-extra-files
...
Add docs, stack.yaml and benchmarks to idris.cabal
2015-09-06 19:42:51 +02:00
Niklas Larsson
5d6a5c41eb
Merge pull request #2579 from suhr/explit-codegen
...
Avoid confusion between the compiler and codegens
2015-09-06 19:42:20 +02:00
Edwin Brady
5be9e7cdb0
Fix parameter propagation
...
This can affect functions which use type synonyms. Fixes #2389
2015-09-06 18:11:52 +01:00
Edwin Brady
5f47887822
Combine a chunk of regxxx tests
...
Now reg001 contains lots of the tests which are only intended to check
whether some code type checks. More to do like this...
2015-09-06 14:52:50 +01:00
Edwin Brady
2f9d287d07
Implicit fix
...
If we normalise the goal type before coercion, we also need to check
against the normalised coercion type otherwise we might miss some valid
coercions. Fixes #2570
2015-09-06 13:52:21 +01:00
Edwin Brady
fcba396622
Coverage checker fix
...
Make sure it looks at all arguments - sometimes applications are nested
by the elaborator and these should be flattened. Fixes #2129
2015-09-06 13:28:57 +01:00
Edwin Brady
c931eff0ba
Proof search improvements
...
Postpone failing searches rather than giving up immediately, since more
information (e.g. type class constraints) may be available when trying
later.
Also improves error reporting of postponed searches by recording what
was being elaborated at the time.
Fixes #2456
2015-09-06 12:48:52 +01:00
