git.iko.soy
/
Idris-dev
readme
files
commits
refs
on
master
help
sign in
history of
4ed62cc..master
compare
1931f0b
Build LLVM rts at the right stage and clean up a namespace
Benjamin Saunders
13 years ago
1945adf
Integers of fixed width should use unsigned comparisons
Benjamin Saunders
13 years ago
8a53e68
Add Functor, Applicative and Monad instances for (Vect n)
Melvar Chen
13 years ago
61d39da
Swapped Vect arguments So now nicer to write type class instances for Functor, Applicative, etc
Edwin Brady
13 years ago
844837c
Going to leave the llvm-general constraint until it's obviously fixed
Edwin Brady
13 years ago
64cf6d2
Merge branch 'Z' of https://github.com/raichoo/Idris-dev into raichoo-Z
Edwin Brady
13 years ago
2972b75
Merge pull request #418 from melted/setup-fix
Edwin Brady
13 years ago
6f21e10
Apparently llvm-general is fixed now
Edwin Brady
13 years ago
9ae048e
Change llvm-general dependency (latest version breaks build)
Edwin Brady
13 years ago
2e8904d
Much faster coverage checking by ignorng forced arguments No need to generate cases to check for them, because we already know their value is forced by another part of the same constructor!
Edwin Brady
13 years ago
83956b4
Minor problem with previous coverage checker patch fixed
Edwin Brady
13 years ago
b8bba09
Speed improvement for coverage checking Lots of repeated work in checking repeated clauses chopped out (there's more of this to come)
Edwin Brady
13 years ago
faf04f3
rename fO into fZ
raichoo
13 years ago
2311d55
rename O into Z
raichoo
13 years ago
fa80591
Fix let scope leakage bug
Edwin Brady
13 years ago
c330406
rename Data.Z into Data.ZZ to avoid name collisions
raichoo
13 years ago
6f88ecd
Add syntax for transformation rules %transform lhs ==> rhs Unbound names on the lhs are treated as patterns. Transformation behaviour not yet implemented.
Edwin Brady
13 years ago
adf646e
Change default specialisation behaviour to not unfold names
Edwin Brady
13 years ago
5dbafdc
Various logging tweaks Just altering some levels to get more useful debugging out of case block elaboration and coverage checking
Edwin Brady
13 years ago
2a1c9d8
LLVM test should return True if no flag is present
Niklas Larsson
13 years ago
ad66486
Add %specialise annotation for functions (Part 1 of partial evaluation) %specialise [n1 t1, n2 t2 ...] as an annotation before a function type means that the r.h.s. of all the clauses will be evaluated, but with the name n1 reduced at most t1 times, etc. The t1 part is optional, and means unlimited (which is the default for all names at the minute anyway)
Edwin Brady
13 years ago
10c9385
Merge pull request #417 from Ralith/bigint-shifts
Edwin Brady
13 years ago
229070c
Merge pull request #415 from Ralith/fix-bigint-division
Edwin Brady
13 years ago
783ef7c
Merge pull request #414 from startling/for-ghci
Edwin Brady
13 years ago
dd51bf7
StrRev primitive too
Benjamin Saunders
13 years ago
a4325c0
Left and arithmetic right shifts on big integers under LLVM codegen
Benjamin Saunders
13 years ago
c2efadd
APPLY needs a catch all case for type constructors Normally, they get erased, but in case they haven't at compile time this ensures they are at run-time. It's safe just to return an erased term since it can't be inspected. Fixes #416 (This may mean something is wrong in erasure, or it may simply be that something is sufficiently higher order that the unused argument checker doesn't feel it is safe to erase.)
Edwin Brady
13 years ago
6b5cb4c
Fix interpreter implementation of signed operations on Integer
Benjamin Saunders
13 years ago
f93c0c0
Added .ghci specifying language extensions.
startling
13 years ago
e09950a
default case for hostDynamicLibExt.
startling
13 years ago
7427990
Merge pull request #404 from Ralith/llvm-fixes
Edwin Brady
13 years ago
a6e3f09
Special case for displaying Type : Type 1 ...because people get the wrong impression about universes otherwise!
Edwin Brady
13 years ago
1c1ad77
Fix LLVM codegen integer interconversion and integer <-> character primitives
Benjamin Saunders
13 years ago
0b25ad1
Change default Num typeclass to integer Fixes #391
Edwin Brady
13 years ago
4bd5a5b
Small coverage checker fix Need to generate possible cases by looking at the patterns, not by looking at the function type alone. Of course, this is what it was trying to do, but there was a mistake... Fixes #397
Edwin Brady
13 years ago
c0ff0e8
Fix type class index propagation bug ...which lead to implicit arguments not being spotted. Fixes #402
Edwin Brady
13 years ago
1d3486f
Merge pull request #400 from JanBessai/JavaRTSOnMavenCentral
Edwin Brady
13 years ago
3b15bf7
Merge branch 'master' of github.com:edwinb/Idris-dev
Edwin Brady
13 years ago
b543b29
Allow names to be attached to provisional definitions lhs ?= {name} rhs -- generates a lemma called 'name' which makes the types of the lhs and rhs match. {name} is optional - a unique name is generated if it is absent.
Edwin Brady
13 years ago
89caf4f
Merge pull request #401 from Ralith/vector-type-completion
Edwin Brady
13 years ago
fcb66ca
Merge pull request #399 from raichoo/vim
Edwin Brady
13 years ago
9376b73
vim: catch user errors
raichoo
13 years ago
c404489
Add primitive vector types to REPL autocompletion
Benjamin Saunders
13 years ago
5d5c613
Remove java rts from idris.cabal
Jan Bessai
13 years ago
c5d5884
Remove Java RTS build in favor of the version hosted on Maven Central
Jan Bessai
13 years ago
67445f5
vim: catch more errors with syntastic
raichoo
13 years ago
ba42979
vim: added syntastic support
raichoo
13 years ago
f7c7a81
Merge branch 'master' of github.com:edwinb/Idris-dev
Edwin Brady
13 years ago
0b5bd21
Merge pull request #398 from hannesm/ideslave-prover
Edwin Brady
13 years ago
e5b36d8
Merge pull request #396 from melted/usage
Edwin Brady
13 years ago
newer commits
older commits
keys
esc to close
j k
move down, up
enter
open
esc
back, or up a level
1 2 3 4
readme, files, commits, refs
/
filter
y
copy the clone command
c
compare the chosen commit with another (or shift-click both)
?
show or hide this list