michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
lean2/tests/lean
History
Leonardo de Moura edcbe6fe10 feat(frontends/lean): allow multiple coercions from class A to B, closes #187 
See new tests (for examples)
tests/lean/run/coe10.lean
tests/lean/run/coe11.lean
tests/lean/run/coe9.lean

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-14 12:59:43 -07:00
..
expensive chore(tests/lean): add 'expensive' file 2014-08-01 10:35:32 -07:00
hott chore(build): remove hott library directory, and move hott tests 2014-08-15 13:30:56 -07:00
interactive fix(frontends/lean/parser): segmentation fault after REPLACE, fixes #172 2014-09-10 08:39:39 -07:00
run feat(frontends/lean): allow multiple coercions from class A to B, closes #187 2014-09-14 12:59:43 -07:00
slow refactor(library): add namespaces 'or', 'and' and 'iff' 2014-09-04 21:25:21 -07:00
alias.lean feat(frontends/lean): rename 'using' command to 'open' 2014-09-03 16:00:38 -07:00
alias.lean.expected.out feat(frontends/lean): add basic pretty printer 2014-07-09 01:12:36 -07:00
bug1.lean feat(frontends/lean/notation_cmd): make the notation for setting precedence uniform 2014-07-01 16:55:41 -07:00
bug1.lean.expected.out chore(kernel/error_msgs): change type mismatch error messages, closes #33 2014-08-07 16:18:40 -07:00
calc1.lean feat(frontends/lean/notation_cmd): make the notation for setting precedence uniform 2014-07-01 16:55:41 -07:00
calc1.lean.expected.out fix(frontends/lean/elaborator): use preprocessed expression when displaying errors 2014-07-29 14:25:50 -07:00
choice_expl.lean feat(frontends/lean): rename 'using' command to 'open' 2014-09-03 16:00:38 -07:00
choice_expl.lean.expected.out fix(frontends/lean): distribute '@' over choice 2014-08-27 16:31:18 -07:00
config.lean chore(tests/lean): reactivate config.lean 2014-07-10 23:32:23 +01:00
config.lean.expected.out chore(shell): re-activate .lean tests 2014-06-11 14:36:42 -07:00
crash.lean fix(tests/lean): adjust test to reflect recent changes 2014-08-26 09:12:18 -07:00
crash.lean.expected.out chore(kernel/error_msgs): change type mismatch error messages, closes #33 2014-08-07 16:18:40 -07:00
ctxopt.lean fix(frontends/lean/parser): configuration options defined in a context are transient, fixes #162 2014-09-09 11:02:54 -07:00
ctxopt.lean.expected.out fix(frontends/lean/parser): configuration options defined in a context are transient, fixes #162 2014-09-09 11:02:54 -07:00
empty.lean feat(frontends/lean): rename 'using' command to 'open' 2014-09-03 16:00:38 -07:00
empty.lean.expected.out feat(frontends/lean/placeholder_elaborator): perform class-instance resolution in a completely independent unifier object, it also triggers the resolution when expected type does not contain metavariables, closes #175, closes #173, closes #68 2014-09-11 14:49:35 -07:00
empty_thm.lean feat(frontends/lean): rename 'using' command to 'open' 2014-09-03 16:00:38 -07:00
empty_thm.lean.expected.out fix(frontends/lean/decl_cmds): improve error message for invalid end of theorem 2014-08-17 17:03:54 -07:00
have1.lean feat(frontends/lean): rename '[fact]' to '[visible]' 2014-09-08 07:47:42 -07:00
have1.lean.expected.out feat(frontends/lean): rename '[fact]' to '[visible]' 2014-09-08 07:47:42 -07:00
let1.lean feat(frontends/lean): rename '[fact]' to '[visible]' 2014-09-08 07:47:42 -07:00
let1.lean.expected.out fix(frontends/lean/pp): pretty print 'let-expressions', closes #87 2014-08-28 18:20:58 -07:00
let3.lean feat(frontends/lean/inductive_cmd): prefix introduction rules with the name of the inductive datatype 2014-09-04 17:26:36 -07:00
let3.lean.expected.out feat(frontends/lean/pp): improve let-expr pretty printer 2014-08-29 07:46:58 -07:00
let4.lean feat(frontends/lean/inductive_cmd): prefix introduction rules with the name of the inductive datatype 2014-09-04 17:26:36 -07:00
let4.lean.expected.out fix(frontends/let): let-expression pretty printer 2014-08-29 10:58:27 -07:00
num.lean feat(frontends/lean/inductive_cmd): prefix introduction rules with the name of the inductive datatype 2014-09-04 17:26:36 -07:00
num.lean.expected.out feat(frontends/lean/pp): pretty print numerals 2014-08-14 09:12:22 -07:00
pp.lean fix(frontends/lean/pp): bug when pretty printing binder information, fixes #73 2014-08-21 09:28:07 -07:00
pp.lean.expected.out feat(frontends/lean): remove restriction on implict arguments, add new test that demonstrates the new feature 2014-09-07 12:29:32 -07:00
protected.lean feat(frontends/lean): rename 'using' command to 'open' 2014-09-03 16:00:38 -07:00
protected.lean.expected.out feat(frontends/lean): add '[protected]' modifier 2014-09-03 15:01:13 -07:00
show1.lean feat(frontends/lean): rename '[fact]' to '[visible]' 2014-09-08 07:47:42 -07:00
show1.lean.expected.out feat(frontends/lean): rename '[fact]' to '[visible]' 2014-09-08 07:47:42 -07:00
showenv.l chore(*): cleanup lean builtin symbols, replace :: with _ 2014-01-09 08:33:52 -08:00
t1.lean refactor(*): rename Bool to Prop 2014-07-22 09:43:18 -07:00
t1.lean.expected.out refactor(*): rename Bool to Prop 2014-07-22 09:43:18 -07:00
t2.lean feat(frontends/lean/builtin_cmds): add simple 'print' command 2014-06-11 14:35:34 -07:00
t2.lean.expected.out feat(frontends/lean/builtin_cmds): add simple 'print' command 2014-06-11 14:35:34 -07:00
t3.lean feat(library/scoped_ext): force user to end a scope with an identifier matching the one used in beginning of scope, closes #30 2014-08-07 16:59:08 -07:00
t3.lean.expected.out feat(frontends/lean): add declaration to namespace without opening it, closes #161 2014-09-09 18:02:14 -07:00
t4.lean feat(library/scoped_ext): force user to end a scope with an identifier matching the one used in beginning of scope, closes #30 2014-08-07 16:59:08 -07:00
t4.lean.expected.out feat(frontends/lean): change the name resolution rules: when in a namespace N that defines C, then C always refers to N.C (i.e., it overrides any alias) 2014-08-18 18:58:50 -07:00
t5.lean feat(library/scoped_ext): force user to end a scope with an identifier matching the one used in beginning of scope, closes #30 2014-08-07 16:59:08 -07:00
t5.lean.expected.out feat(frontends/lean): add basic pretty printer 2014-07-09 01:12:36 -07:00
t6.lean refactor(*): rename Bool to Prop 2014-07-22 09:43:18 -07:00
t6.lean.expected.out refactor(*): rename Bool to Prop 2014-07-22 09:43:18 -07:00
t7.lean refactor(*): rename Bool to Prop 2014-07-22 09:43:18 -07:00
t7.lean.expected.out feat(frontends/lean): remove restriction on implict arguments, add new test that demonstrates the new feature 2014-09-07 12:29:32 -07:00
t9.lean feat(library/scoped_ext): force user to end a scope with an identifier matching the one used in beginning of scope, closes #30 2014-08-07 16:59:08 -07:00
t9.lean.expected.out fix(tests/lean): adjust tests expected output 2014-08-13 12:35:14 -07:00
t10.lean feat(frontends/lean/notation_cmd): make the notation for setting precedence uniform 2014-07-01 16:55:41 -07:00
t10.lean.expected.out chore(kernel/error_msgs): change type mismatch error messages, closes #33 2014-08-07 16:18:40 -07:00
t11.lean feat(frontends/lean/notation_cmd): add 'notation' command 2014-06-15 10:49:05 -07:00
t11.lean.expected.out feat(frontends/lean): add basic pretty printer 2014-07-09 01:12:36 -07:00
t12.lean feat(frontends/lean): add local notation support 2014-06-15 11:30:52 -07:00
t12.lean.expected.out feat(frontends/lean): add basic pretty printer 2014-07-09 01:12:36 -07:00
t13.lean feat(frontends/lean): local notation 'shadows' global one 2014-06-15 11:50:41 -07:00
t13.lean.expected.out feat(frontends/lean): add basic pretty printer 2014-07-09 01:12:36 -07:00
t14.lean feat(frontends/lean): rename 'using' command to 'open' 2014-09-03 16:00:38 -07:00
t14.lean.expected.out feat(frontends/lean): add 'export' command 2014-09-03 18:37:01 -07:00
test.sh refactor(library): remove unnecessary 'standard' subdirectory 2014-08-23 18:08:09 -07:00
test_single.sh refactor(library): remove unnecessary 'standard' subdirectory 2014-08-23 18:08:09 -07:00
test_single_pp.sh chore(tests): cleanup test scripts 2014-06-29 09:03:39 -07:00
uni_bug1.lean feat(frontends/lean): rename 'using' command to 'open' 2014-09-03 16:00:38 -07:00
uni_bug1.lean.expected.out fix(library/unifier): we should preprocess choice constraints before we start solving any constraint, fixes #85 2014-08-21 16:58:25 -07:00