4* Agda-style equational reasoning (in Syntax.PreorderReasoning)
5* 'case' construct now abstracts over the scrutinee in its type
6* Added label type 'name (equivalent to the empty type).
7 This is intended for field/effect disambiguation. "name" can be any
8 valid identifier. Two labels are definitionally equal if they have the
19* Type classes now implemented as dependent records, meaning that method
20 types may now depend on earlier methods.
21* More flexible class instance resolution, so that function types and lambda
22 expressions can be made instances of a type class.
23* Add !expr notation for implicit binding of intermediate results in
24 monadic/do/etc expressions.
25* Extend Effects package to cope with possibly failing operations, using
26 "if_valid", "if_error", etc.
27* At the REPL, "it" now refers to the previous expression.
28* Semantic colouring at the REPL. Turn this off with --nocolour.
29* Some prettifying of error messages.
30* The contents of ~/.idris/repl/init are run at REPL start-up.
31* The REPL stores a command history in ~/.idris/repl/history.
32* The [a..b], [a,b..c], [a..], and [a,b..] syntax now pass the totality
33 checker and can thus be used in types. The [x..] syntax now returns an
34 actually infinite stream.
35* Add '%reflection' option for functions, for compile-time operations on
37* Add expression form 'quoteGoal x by p in e' which applies p to the expected
38 expression type and binds the result to x in the scope e.
39* Performance improvements in Strings library.
40* Library reorganisation, separated into prelude/ and base/.
44* New module/dependency tree checking.
45* New parser implementation with more precise errors.
46* Improved type class resolution.
47* Compiling Nat via GMP integers.
48* Performance improvements in elaboration.
49* Improvements in termination checking.
50* Various REPL commands to support interactive editing, and a client/server
51 mode to allow external invocation of REPL commands.
56* Apply functions by return type, rather than with arguments:
57 "t <== f" means "apply f with arguments such that it returns a value
59* Allow the result type of a rewrite to be specified
60* Allow names to be attached to provisional definitions
61 lhs ?= {name} rhs -- generates a lemma called 'name' which makes the
62 types of the lhs and rhs match. {name} is optional - a unique name is
63 generated if it is absent.
64* Experimental LLVM backend
65* Added Data.HVect module
66* Fix fromInteger to take an Integer, rather than an Int
67* Integer literals for Fin
68* Renamed O to Z, and fO to fZ
69* Swapped Vect arguments, now Vect : Nat -> Type -> Type
70* Added DecEq instances
71* Add 'equiv' tactic, which rewrites a goal to an equivalent (convertible) goal
75* Add annotation for unification traces
76* Add 'mrefine' tactic for refining by matching against a type
77* Type class resolution fixes
78* Much faster coverage checking
85* Added "rewrite ... in ..." construct
86* Allow type class constraints in 'using' clauses
87* Renamed EFF to EFFECT in Effect package
88* Experimental Java backend
89* Tab completion in REPL
90* Dynamic loading of C libraries in the interpreter
91* Testing IO actions at the REPL with :x command
92* Improve rendering of :t
93* Fixed some INTERNAL ERROR messages
97* Fix non-linear pattern checking
98* Improved name disambiguation
99* More flexible unification and elaboration of lambdas
100* Various unification and totality checking bug fixes
107* 'implicit' keyword, for implicit type conversion
108* Added Effects package
109* Primitives for 8,16,32 and 64 bit integers
113* Change unification so that it keeps track of failed constraints in case
114 later information helps to resolve them
115* Distinguishing parameters and indices in data types
116* Faster termination/coverage checking
117* Split 'javascript' target into 'javascript' and 'node'
124* The type of types is now 'Type' rather than 'Set'
125* Forward declarations of data allowed
126 - supporting induction recursion and mutually recursive data
127* Type inference of definitions in 'where' clauses
128 - Provided that the type can be completely determined from the first
129 application of the function (in the top level definition)
130* 'mutual' blocks added
131 - effect is to elaborate all types of declarations in the block before
132 elaborating their definitions
133 - allows inductive-recursive definitions
134* Expression inspected by 'with' clause now abstracted from the goal
136* Implicit arguments will be added automatically only if their initial
137 letter is lower case, or they are in a using declaration
138* Added documentation comments (Haddock style) and ':doc' REPL command
139* Pattern matching on strings, big integers and characters
140* Added System.Concurrency modules
141* Added 'postulate' declarations
142* Allow type annotations on 'let' tactic
143* EXPERIMENTAL JavaScript generation, with '--target javascript' option
147* Separate inlining methods at compile-time and run-time
148* Fixed nested parameters blocks
149* Improve efficiency of elaborator by:
150 - only normalising when necessary
151 - reducing backtracking with resolving ambiguities
152* Better compilation of case trees
160 - as data declarations, but constructor arguments are evaluated lazily
161 - functions which return a codata type do not reduce at compile time
162* Added 'parameters' blocks
163* Allow local data definitions in where blocks
164* Added '%default' directive to declare total-by-default or partial-by-default
165 for functions, and a corresponding "partial" reserved words to mark functions
166 as allowed to be partial. Also "--total" and "--partial" added as command
168* Command line option "--warnpartial" for flagging all undeclared
169 partial functions, without error.
170* New termination checker supporting mutually recursive definitions.
171* Added ':load' command to REPL, for loading a new file
172* Added ':module' command to REPL, for adding modules
173* Renamed library modules (now have initial capital)
177* Several improvements and fixes to unification
178* Added collapsing optimisation and more aggressive erasure
185* Simple packaging system
186* Added --dumpc flag for displaying generated code
190* Improve overloading resolution (especially where this is a type error)
191* Various important bug fixes with evaluation and compilation
192* More aggressive compile-time evaluation
199* Added binding forms to syntax rules
200* Named class instances
201* Added ':set' command, with options 'errorcontext' for displaying local
202 variables in scope when a unification error occurs, and 'showimplicits'
203 for displaying elaborated terms in full
204* Added '--errorcontext' command line switch
205* Added ':proofs' and ':rmproofs' commands
206* Various minor REPL improvements and fixes
210* Completely new run time system (not based on Epic or relying on Boehm GC)
211* Normalise before forcing to catch more forceable arguments
212* Types no longer exported in normal form
213* Try to resolve overloading by inspecting types, rather than full type
221* backtick notation added: x `foo` y ==> foo x y
222* case expressions allowed in type signatures
223* Library extensions in prelude.vect and prelude.algebra
224* malloc/trace_malloc added to builtins.idr
228* Some type class resolution fixes
229* Several minor bug fixes
230* Performance improvements in resolving overloading and type classes
237* DSL notation, for overloading lambda and let bindings
238* Dependent records, with projection and update
239* Totality checking and 'total' keyword
240* Auto implicits and default argument values {auto n : T}, {default val n : T}
241* Overlapping type class instances disallowed
242* Many extensions to prelude.nat and prelude.list libraries (mostly thanks to
244* New libraries: control.monad.identity, control.monad.state
245* Small improvements in error reporting
249* Faster compilation (only compiling names which are used)
250* Better type class resolution
251* Lots of minor bug fixes
255Complete rewrite. User visible changes:
257* New proof/tactics syntax
258* New syntax for pairs/dependent pairs
259* Indentation-significant syntax
262* Added case expressions, pattern matching let and lambda
263* Added monad comprehensions
264* Added cumulativity and universe checking
265* Ad-hoc name overloading
266 - Resolved by type or explicit namespace
267* Modules (Haskell-style)
268* public, abstract and private access to functions and types
269* Separate type-checking
270* Improved interactive environment
271* Replaced 'do using' with Monad class
272* Extended syntax macros
277* All definitions (functions, classes and instances) are elaborated to top
278 level, fully explicit, data declarations and pattern matching definitions,
279 which are verified by a minimal type checker.
281This is the first release of a complete reimplementation. There will be bugs.
282If you find any, please do not hesitate to contact Edwin Brady
283(ecb10@st-andrews.ac.uk).
keysesc 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