lean2/tests/lean
Leonardo de Moura 4c67721d32 Fix test error on Cygwin
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-09 18:35:11 -07:00
..
bad Add more 'bad' examples 2013-09-09 09:19:49 -07:00
slow Move 'slow' test files to different subdir. Modify CTestCustom.cmake.in to run leantests. 2013-09-06 08:48:12 -07:00
arith1.lean Fix unit tests for Windows 2013-09-03 10:44:51 -07:00
arith1.lean.expected.out Display the input term in the output of the Check command. It is useful to see the fully elaborated term. 2013-09-08 22:55:21 -07:00
arith2.lean Add Real arithmetic. Fix elaborator for coercions. Now, two overloads are considered ambiguous if they need the same number of coercions. Improve pretty printer for nest infix operators with same precedence and associativity. 2013-09-02 13:20:00 -07:00
arith2.lean.expected.out Fix unit tests for Windows 2013-09-03 10:44:51 -07:00
arith3.lean Fix unit tests for Windows 2013-09-03 10:44:51 -07:00
arith3.lean.expected.out Fix unit tests for Windows 2013-09-03 10:44:51 -07:00
arith4.lean Add trigonometric functions 2013-09-02 17:03:02 -07:00
arith4.lean.expected.out Fix unit tests for Windows 2013-09-03 10:44:51 -07:00
arith5.lean Add hyperbolic functions 2013-09-02 17:28:43 -07:00
arith5.lean.expected.out Fix unit tests for Windows 2013-09-03 10:44:51 -07:00
arith6.lean Define divides, and add examples 2013-09-03 20:18:20 -07:00
arith6.lean.expected.out Define divides, and add examples 2013-09-03 20:18:20 -07:00
arith7.lean Define absolute value function and notation for it. Add new example. 2013-09-03 20:39:54 -07:00
arith7.lean.expected.out Add unicode name for the types: Nat, Int and Real 2013-09-04 09:03:41 -07:00
arith8.lean Parse decimal values 2013-09-06 08:48:12 -07:00
arith8.lean.expected.out Parse decimal values 2013-09-06 08:48:12 -07:00
arrow.lean Improve pretty printer for Pi's 2013-09-08 11:04:07 -07:00
arrow.lean.expected.out Improve pretty printer for Pi's 2013-09-08 11:04:07 -07:00
cast1.lean Add Cast, DomInj and RanInj. Improve operator << for lean_frontend objects. 2013-09-06 18:32:15 -07:00
cast1.lean.expected.out Display the input term in the output of the Check command. It is useful to see the fully elaborated term. 2013-09-08 22:55:21 -07:00
cast2.lean Add Cast, DomInj and RanInj. Improve operator << for lean_frontend objects. 2013-09-06 18:32:15 -07:00
cast2.lean.expected.out Display the input term in the output of the Check command. It is useful to see the fully elaborated term. 2013-09-08 22:55:21 -07:00
cast3.lean Add casting propagation and normalization 2013-09-06 20:45:26 -07:00
cast3.lean.expected.out Display the input term in the output of the Check command. It is useful to see the fully elaborated term. 2013-09-08 22:55:21 -07:00
coercion1.lean Fix unit tests for Windows 2013-09-03 10:44:51 -07:00
coercion1.lean.expected.out Fix unit tests for Windows 2013-09-03 10:44:51 -07:00
coercion2.lean Fix unit tests for Windows 2013-09-03 10:44:51 -07:00
coercion2.lean.expected.out Fix test error on Cygwin 2013-09-09 18:35:11 -07:00
config.lean Fix unit tests for Windows 2013-09-03 10:44:51 -07:00
config.lean.expected.out Fix unit tests for Windows 2013-09-03 10:44:51 -07:00
elab1.lean Improve elaborator error messages 2013-09-04 16:36:58 -07:00
elab1.lean.expected.out Improve pretty printer for Pi's 2013-09-08 11:04:07 -07:00
elab2.lean Fix bug in the elaborator. Move character ' to class A 2013-09-06 17:12:35 -07:00
elab2.lean.expected.out Fix bug in the elaborator. Move character ' to class A 2013-09-06 17:12:35 -07:00
elab3.lean Add missing case to elaborator 2013-09-06 17:43:08 -07:00
elab3.lean.expected.out Add missing case to elaborator 2013-09-06 17:43:08 -07:00
elab4.lean Fix problem with pretty printer. Add another test for elaborator 2013-09-06 18:01:11 -07:00
elab4.lean.expected.out Keep expanded form when pretty printings variable declarations with implicit marks (i.e., curly braces) 2013-09-08 11:23:46 -07:00
elab5.lean Display the input term in the output of the Check command. It is useful to see the fully elaborated term. 2013-09-08 22:55:21 -07:00
elab5.lean.expected.out Display the input term in the output of the Check command. It is useful to see the fully elaborated term. 2013-09-08 22:55:21 -07:00
ex1.lean Add test script 2013-08-31 18:31:39 -07:00
ex1.lean.expected.out Fix unit tests for Windows 2013-09-03 10:44:51 -07:00
ex2.lean Fix unit tests for Windows 2013-09-03 10:44:51 -07:00
ex2.lean.expected.out Improve application type mismatch errors. We also show the implicit arguments (not just their types) 2013-09-04 16:36:58 -07:00
ex3.lean Fix unit tests for Windows 2013-09-03 10:44:51 -07:00
ex3.lean.expected.out Improve pretty printer for Pi's 2013-09-08 11:04:07 -07:00
implicit1.lean Modify the parser for accepting expressions such as: 'fun a b, f a b', 'forall a, f a > 0', etc. This is just syntax sugar for 'fun (a : _) (b : _), f a b' and 'forall a : _, f a > 0' 2013-09-03 17:24:05 -07:00
implicit1.lean.expected.out Add unicode name for the types: Nat, Int and Real 2013-09-04 09:03:41 -07:00
let1.lean Add (optional) type to let declarations 2013-09-06 10:06:26 -07:00
let1.lean.expected.out Display the input term in the output of the Check command. It is useful to see the fully elaborated term. 2013-09-08 22:55:21 -07:00
let2.lean Add (optional) type to let declarations 2013-09-06 10:06:26 -07:00
let2.lean.expected.out Add (optional) type to let declarations 2013-09-06 10:06:26 -07:00
let3.lean Add (optional) type to let declarations 2013-09-06 10:06:26 -07:00
let3.lean.expected.out Add (optional) type to let declarations 2013-09-06 10:06:26 -07:00
let4.lean Fix type checker and elaborator for let expressions. Fix get_coercions (we need to pass the context). Fix pretty printer for def_type_mismatch_exception. 2013-09-06 11:02:00 -07:00
let4.lean.expected.out Display the input term in the output of the Check command. It is useful to see the fully elaborated term. 2013-09-08 22:55:21 -07:00
overload1.lean Add support for overloads in the elaborator 2013-09-01 14:54:02 -07:00
overload1.lean.expected.out Fix unit tests for Windows 2013-09-03 10:44:51 -07:00
overload2.lean Fix unit tests for Windows 2013-09-03 10:44:51 -07:00
overload2.lean.expected.out Add unicode name for the types: Nat, Int and Real 2013-09-04 09:03:41 -07:00
test.sh Fix unit tests for Windows 2013-09-03 10:44:51 -07:00
tst1.lean Fix unit tests for Windows 2013-09-03 10:44:51 -07:00
tst1.lean.expected.out Display the input term in the output of the Check command. It is useful to see the fully elaborated term. 2013-09-08 22:55:21 -07:00
tst2.lean Move files in examples directory to tests directory. They are not real examples 2013-08-31 19:16:30 -07:00
tst2.lean.expected.out Fix unit tests for Windows 2013-09-03 10:44:51 -07:00
tst3.lean Fix unit tests for Windows 2013-09-03 10:44:51 -07:00
tst3.lean.expected.out Fix unit tests for Windows 2013-09-03 10:44:51 -07:00
tst4.lean Fix unit tests for Windows 2013-09-03 10:44:51 -07:00
tst4.lean.expected.out Fix test error on Cygwin 2013-09-09 18:35:11 -07:00
tst5.lean Fix unit tests for Windows 2013-09-03 10:44:51 -07:00
tst5.lean.expected.out Display the input term in the output of the Check command. It is useful to see the fully elaborated term. 2013-09-08 22:55:21 -07:00
tst6.lean Fix unit tests for Windows 2013-09-03 10:44:51 -07:00
tst6.lean.expected.out Fix problem with pretty printer. Add another test for elaborator 2013-09-06 18:01:11 -07:00
tst7.lean Fix unit tests for Windows 2013-09-03 10:44:51 -07:00
tst7.lean.expected.out Display the input term in the output of the Check command. It is useful to see the fully elaborated term. 2013-09-08 22:55:21 -07:00
tst8.lean Add missing test 2013-09-03 14:51:34 -07:00
tst8.lean.expected.out Display the input term in the output of the Check command. It is useful to see the fully elaborated term. 2013-09-08 22:55:21 -07:00
tst9.lean Fix unit tests for Windows 2013-09-03 10:44:51 -07:00
tst9.lean.expected.out Improve application type mismatch errors. We also show the implicit arguments (not just their types) 2013-09-04 16:36:58 -07:00
tst10.lean Fix unit tests for Windows 2013-09-03 10:44:51 -07:00
tst10.lean.expected.out Display the input term in the output of the Check command. It is useful to see the fully elaborated term. 2013-09-08 22:55:21 -07:00
tst11.lean Fix unit tests for Windows 2013-09-03 10:44:51 -07:00
tst11.lean.expected.out Display the input term in the output of the Check command. It is useful to see the fully elaborated term. 2013-09-08 22:55:21 -07:00
tst12.lean Fix unit tests for Windows 2013-09-03 10:44:51 -07:00
tst12.lean.expected.out Fix unit tests for Windows 2013-09-03 10:44:51 -07:00
tst13.lean Fix unit tests for Windows 2013-09-03 10:44:51 -07:00
tst13.lean.expected.out Fix unit tests for Windows 2013-09-03 10:44:51 -07:00
tst14.lean Fix unit tests for Windows 2013-09-03 10:44:51 -07:00
tst14.lean.expected.out Display the input term in the output of the Check command. It is useful to see the fully elaborated term. 2013-09-08 22:55:21 -07:00
tst15.lean Fix unit tests for Windows 2013-09-03 10:44:51 -07:00
tst15.lean.expected.out Display the input term in the output of the Check command. It is useful to see the fully elaborated term. 2013-09-08 22:55:21 -07:00
tst16.lean Fix unit tests for Windows 2013-09-03 10:44:51 -07:00
tst16.lean.expected.out Display the input term in the output of the Check command. It is useful to see the fully elaborated term. 2013-09-08 22:55:21 -07:00
tst17.lean Fix unit tests for Windows 2013-09-03 10:44:51 -07:00
tst17.lean.expected.out Display the input term in the output of the Check command. It is useful to see the fully elaborated term. 2013-09-08 22:55:21 -07:00
unicode.lean Fix unit tests for Windows 2013-09-03 10:44:51 -07:00
unicode.lean.expected.out Fix unit tests for Windows 2013-09-03 10:44:51 -07:00
vars1.lean Add 'Variables' command. 2013-09-06 08:48:12 -07:00
vars1.lean.expected.out Add 'Variables' command. 2013-09-06 08:48:12 -07:00