Idris-dev/test/README

Tests:

001: Well-typed interpreter
002: Universe checking
003: Literate source and string processing
004: File operations
005: Num class resolution [regression]; span & break; ad-hoc overloading
006: Provisional definitions; class resolution in patterns
007: Applicative and idiom brackets
008: case and pattern matching let
009: ranges and list monad
010: total
011: record projection and update
012: various error regressions
013: binding syntax
014: resource DSL
015: verified binary adder
016: codata

regxxx: various regression tests
Fix obscure where naming bug 2011-12-22 02:06:26 +04:00			`Tests:`

			`001: Well-typed interpreter`
			`002: Universe checking`
			`003: Literate source and string processing`
			`004: File operations`
			`005: Num class resolution [regression]; span & break; ad-hoc overloading`
New test 2012-01-01 23:59:46 +04:00			`006: Provisional definitions; class resolution in patterns`
Test for idiom brackets and Applicative class 2012-01-04 15:05:37 +04:00			`007: Applicative and idiom brackets`
Added case and pattern matching let bindings Also pattern matching bind in do notation case notation currently has limitations: - only works on simple types (each pattern must have the same type, more specifically) - return type needs to be known at the point of elaboration 2012-01-06 04:10:12 +04:00			`008: case and pattern matching let`
Numeric ranges [a..b], [a,b .. c] and list monad 2012-01-06 19:11:11 +04:00			`009: ranges and list monad`
Added record test 2012-01-28 01:21:31 +04:00			`010: total`
			`011: record projection and update`
Check patterns are inaccessible 2012-04-24 17:57:55 +04:00			`012: various error regressions`
Added binding form to syntax rules (and updated tutorial accordingly) 2012-05-30 13:32:57 +04:00			`013: binding syntax`
Warn when generating a setter for a record fails ...rather than failing (since it may just not work for dependent records) 2012-10-18 23:52:17 +04:00			`014: resource DSL`
			`015: verified binary adder`
Added simple productivity checker for coinductive definitions Recursive calls must be an argument to a coinductive constructor 2012-10-23 03:37:55 +04:00			`016: codata`
Warn when generating a setter for a record fails ...rather than failing (since it may just not work for dependent records) 2012-10-18 23:52:17 +04:00
			`regxxx: various regression tests`