Henrik Böving 0fde2db75e feat: improve the heuristic for notation delab ... Instead of the previous constraints on the right hand side that only allowed a permutation of variables as parameters to a function the new heuristic allows anything to the right of a function as long as each variable only appears at most once.		2022-06-23 13:27:53 -07:00
..
interactive	feat: show term goal at end of term as well	2022-06-23 14:44:19 +02:00
Reformat	chore: fix tests	2022-06-16 23:33:57 +02:00
run	fix: avoid unnecessary dependencies at mkMatcher	2022-06-23 10:21:32 -07:00
server	fix: unused variables linter review comments	2022-06-03 13:03:52 +02:00
trust0	fix: unused variables linter review comments	2022-06-03 13:03:52 +02:00
.gitignore
217.lean
217.lean.expected.out	feat: show argument name at "don't know how to synthesize placeholder" error messages	2021-12-09 06:48:06 -08:00
220.lean
220.lean.expected.out	feat: add equality proof for named patterns	2022-01-18 12:43:01 -08:00
223.lean	chore: remove ≅ notation for HEq	2021-09-15 08:06:32 -07:00
223.lean.expected.out	chore: fix tests	2021-12-15 11:42:38 +00:00
236.lean	feat: top-down heuristic delaboration	2021-08-03 09:13:18 +02:00
236.lean.expected.out	fix: return fully-qualified name in PrettyPrinter when pp.fullNames is set	2021-11-21 15:23:21 +01:00
241.lean	fix: fixes #241	2021-05-22 19:10:07 -07:00
241.lean.expected.out	fix: fixes #241	2021-05-22 19:10:07 -07:00
242.lean	fix: fixes #242	2021-08-06 18:39:55 -07:00
242.lean.expected.out	fix: fixes #242	2021-08-06 18:39:55 -07:00
243.lean	fix: fixes #243	2021-05-03 13:01:16 -07:00
243.lean.expected.out	feat: improve argument type mismatch error position, and do not stop at application type mismatch errors	2022-04-25 16:30:40 -07:00
247.lean	fix: fixes #247	2021-04-15 12:33:45 -07:00
247.lean.expected.out	fix: no method lift over let	2021-04-24 19:33:55 -07:00
248.lean	chore: fix tests	2022-06-14 17:27:13 -07:00
248.lean.expected.out	chore: fix tests	2022-06-14 17:27:13 -07:00
255.lean	feat: allow hygienic capture of section variables in quotations	2021-01-24 11:46:04 -08:00
255.lean.expected.out	feat: improve the heuristic for notation delab	2022-06-23 13:27:53 -07:00
276.lean	feat: add PEmpty	2021-08-06 19:18:22 -07:00
276.lean.expected.out	feat: add PEmpty	2021-08-06 19:18:22 -07:00
277a.lean	feat: notation: unfold to prechecked quotation	2021-04-27 16:38:37 -07:00
277a.lean.expected.out	chore: show declaration with sorry in #eval	2022-01-17 13:18:22 -08:00
277b.lean	fix: do not evaluate code containing sorry	2021-01-26 15:01:53 -08:00
277b.lean.expected.out	chore: show declaration with sorry in #eval	2022-01-17 13:18:22 -08:00
283.lean	fix: solve method at isLevelDefEq	2021-01-20 08:36:26 -08:00
283.lean.expected.out	feat: improve argument type mismatch error position, and do not stop at application type mismatch errors	2022-04-25 16:30:40 -07:00
297.lean	fix: missing checkAssignment at assignToConstFun	2021-01-26 17:33:33 -08:00
297.lean.expected.out	feat: in pure code, do use assume Id monad at do notation	2021-12-10 12:55:14 -08:00
301.lean	fix: missing occursCheck at SyntheticMVars	2021-01-29 17:13:04 -08:00
301.lean.expected.out	fix: no sorry-warning for missing match cases	2022-06-01 07:41:52 -07:00
302.lean	fix: fixes #302	2021-02-03 15:04:18 -08:00
302.lean.expected.out	fix: addAutoBoundImplicitsOld occurrences at MutualDef.lean and Structure.lean	2022-03-25 09:07:59 -07:00
307.lean	test: for issues #306 and #307	2021-02-06 12:48:43 -08:00
307.lean.expected.out	test: for issues #306 and #307	2021-02-06 12:48:43 -08:00
309.lean	fix: make sure kernel checks examples	2021-02-25 13:34:27 -08:00
309.lean.expected.out	fix: make sure kernel checks examples	2021-02-25 13:34:27 -08:00
331.lean	feat: improve error message	2021-03-05 13:42:54 -08:00
331.lean.expected.out	feat: improve error message	2021-03-05 13:42:54 -08:00
343.lean	fix: universe level parameter stabilitity issue	2022-06-10 14:08:08 -07:00
343.lean.expected.out	chore: fix tests	2022-05-31 18:01:48 -07:00
345.lean	fix: fixes #345	2021-03-11 18:59:39 -08:00
345.lean.expected.out	feat: allow universes metavariables from any depth to be assigned when ignoreLevelDepth is true	2021-08-18 20:20:51 -07:00
346.lean	chore: improve error message	2021-03-16 20:42:38 -07:00
346.lean.expected.out	feat: improve error message produced by #eval command when it fails to synthesize "eval" instance	2021-11-05 15:03:57 -07:00
348.lean	fix: fixes #348	2021-03-16 17:50:40 -07:00
348.lean.expected.out	feat: hide elaboration errors from partial syntax trees by default	2021-04-13 19:24:35 +02:00
353.lean	fix: register new metavariables created when applying default instance	2021-03-16 17:31:51 -07:00
353.lean.expected.out	feat: backtrack when applying default instances if subproblems cannot be solved	2022-05-07 09:56:38 -07:00
361.lean	chore: fix test	2022-01-31 16:45:57 -08:00
361.lean.expected.out	feat: remove space before propositions with inaccessible names	2022-04-07 07:54:50 -07:00
366.lean	fix: fixes #366	2021-03-23 16:02:45 -07:00
366.lean.expected.out	fix: correctly pretty-print @Eq	2022-01-12 09:41:41 +01:00
386.lean	fix: fixes #386	2021-04-11 20:57:39 -07:00
386.lean.expected.out	fix: fixes #386	2021-04-11 20:57:39 -07:00
389.lean	test: expand test for 389	2021-04-11 20:55:33 -07:00
389.lean.expected.out	feat: improve argument type mismatch error position, and do not stop at application type mismatch errors	2022-04-25 16:30:40 -07:00
414.lean	chore: fix tests	2022-04-01 11:34:50 -07:00
414.lean.expected.out	fix: fixes #414	2021-04-19 15:02:26 -07:00
415.lean	feat: closes #415	2021-05-03 18:04:01 -07:00
415.lean.expected.out	feat: pp.analyze detect when struct-inst type needed	2021-08-03 09:13:18 +02:00
421.lean	chore: fix tests	2021-09-16 10:29:38 -07:00
421.lean.expected.out	fix: closes #421	2021-04-23 12:27:39 -07:00
423.lean	test: add second example for issue #423	2021-04-25 10:35:23 -07:00
423.lean.expected.out	feat: improve argument type mismatch error position, and do not stop at application type mismatch errors	2022-04-25 16:30:40 -07:00
435.lean	fix: fixes #435	2021-05-02 18:16:57 -07:00
435.lean.expected.out	chore: fix tests	2022-05-31 18:01:48 -07:00
435b.lean	fix: add basic support for accessing the field of a section variable in the notation prechecker	2021-05-04 22:41:25 -07:00
435b.lean.expected.out	fix: add basic support for accessing the field of a section variable in the notation prechecker	2021-05-04 22:41:25 -07:00
439.lean	fix: correctly pretty-print @Eq	2022-01-12 09:41:41 +01:00
439.lean.expected.out	feat: improve argument type mismatch error position, and do not stop at application type mismatch errors	2022-04-25 16:30:40 -07:00
440.lean	feat: closes #440	2021-05-15 20:54:54 -07:00
440.lean.expected.out	chore: show declaration with sorry in #eval	2022-01-17 13:18:22 -08:00
445.lean	chore: smartUnfolding cleanup	2021-09-19 15:29:11 -07:00
445.lean.expected.out	feat: improve binder names introduced by the match discriminant refinement feature	2022-04-08 06:49:09 -07:00
448.lean	chore: remove tryPureCoe?	2022-02-03 16:25:24 -08:00
448.lean.expected.out	fix: fixes #448	2021-05-10 20:07:28 -07:00
449.lean	fix: fixes #449	2021-05-10 13:10:59 -07:00
449.lean.expected.out	fix: fixes #449	2021-05-10 13:10:59 -07:00
450.lean	fix: fixes #450	2021-05-10 13:55:06 -07:00
450.lean.expected.out	feat: add Lean.Elab.Term.getMVarErrorInfo?	2021-12-09 06:48:06 -08:00
456.lean	fix: fixes #456	2021-05-11 21:07:21 -07:00
456.lean.expected.out	fix: fixes #456	2021-05-11 21:07:21 -07:00
469.lean	fix: check arity in notation unexpander	2021-07-22 16:59:19 +02:00
469.lean.expected.out	fix: check arity in notation unexpander	2021-07-22 16:59:19 +02:00
474.lean	chore: remove tryPureCoe?	2022-02-03 16:25:24 -08:00
474.lean.expected.out	feat: add Meta.abstract	2021-08-06 18:19:06 -07:00
490.lean	fix: _root_ prefix in declarations	2022-06-13 14:03:18 -07:00
490.lean.expected.out	fix: _root_ prefix in declarations	2022-06-13 14:03:18 -07:00
496.lean	chore: improve error message when compiling code containing axioms or noncomputable definitions	2021-05-31 20:27:15 -07:00
496.lean.expected.out	chore: improve error message when compiling code containing axioms or noncomputable definitions	2021-05-31 20:27:15 -07:00
529.lean	feat: add withOpenDecl and withOpen parsers	2021-08-22 20:50:35 -07:00
529.lean.expected.out	feat: add withOpenDecl and withOpen parsers	2021-08-22 20:50:35 -07:00
550.lean	fix: offset support at isDefEq should not use HAdd.hAdd	2021-07-27 16:16:03 -07:00
550.lean.expected.out	fix: offset support at isDefEq should not use HAdd.hAdd	2021-07-27 16:16:03 -07:00
586.lean	fix: ensure hygiene of double-quoted names	2021-07-30 07:17:50 -07:00
586.lean.expected.out	fix: ensure hygiene of double-quoted names	2021-07-30 07:17:50 -07:00
593.lean	fix: fixes #593	2021-08-02 10:46:12 -07:00
593.lean.expected.out	feat: improved name-unresolving in delab	2021-09-07 16:26:00 +02:00
603.lean	feat: borrow inference: preserve mutual tail calls	2021-08-05 06:26:06 -07:00
603.lean.expected.out	feat: add a proper BEq instance for Nat	2022-03-01 09:01:08 -08:00
604.lean	fix: fixes #604	2021-08-04 17:19:17 -07:00
604.lean.expected.out	chore: disable pp.analyze for now	2021-09-07 07:51:43 -07:00
620.lean	fix: fixes #620	2021-08-10 15:06:06 -07:00
620.lean.expected.out	fix: fixes #620	2021-08-10 15:06:06 -07:00
621.lean	fix: fixes #621	2021-08-10 21:15:35 -07:00
621.lean.expected.out	chore: fix tests	2022-01-20 15:25:59 -08:00
625.lean	chore: remove unnecessary args	2022-04-07 18:19:15 -07:00
625.lean.expected.out	fix: appUnexpander name resolution	2021-10-09 08:29:26 -07:00
629.lean	fix: BinomialHeap: insert (head h) (tail h) = h	2021-08-17 10:19:12 -07:00
629.lean.expected.out	fix: BinomialHeap: insert (head h) (tail h) = h	2021-08-17 10:19:12 -07:00
641.lean	feat: improved name-unresolving in delab	2021-09-07 16:26:00 +02:00
641.lean.expected.out	feat: include types in the "ambiguous, possible interpretations" error message	2022-03-06 07:26:31 -08:00
653.lean	fix: fixes #653	2021-09-04 18:42:33 -07:00
653.lean.expected.out	fix: fixes #653	2021-09-04 18:42:33 -07:00
655.lean	fix: fixes #655	2021-09-07 12:17:28 -07:00
655.lean.expected.out	fix: fixes #655	2021-09-07 12:17:28 -07:00
679.lean	chore: remove tryPureCoe?	2022-02-03 16:25:24 -08:00
679.lean.expected.out	fix: fixes #679	2021-09-18 15:34:29 -07:00
689.lean	fix: panic messages on invalid input	2021-09-25 09:01:01 -07:00
689.lean.expected.out	fix: panic messages on invalid input	2021-09-25 09:01:01 -07:00
690.lean	fix: check number of explicit variables at induction/cases alternatives when @ is not used	2021-09-29 07:39:38 -07:00
690.lean.expected.out	chore: fix tests	2022-06-01 06:36:25 -07:00
697.lean	feat: reject partial when if constant is not a function	2021-09-28 21:07:14 -07:00
697.lean.expected.out	feat: reject partial when if constant is not a function	2021-09-28 21:07:14 -07:00
714.lean	feat: make sure #check produces some result even when there are pending TC problems	2021-10-06 13:37:06 -07:00
714.lean.expected.out	feat: make sure #check produces some result even when there are pending TC problems	2021-10-06 13:37:06 -07:00
755.lean	fix: bug at Offset.lean	2021-11-08 18:27:25 -08:00
755.lean.expected.out	chore: fix test	2022-01-20 17:19:29 -08:00
770.lean	feat: in pure code, do use assume Id monad at do notation	2021-12-10 12:55:14 -08:00
770.lean.expected.out	feat: improve do notation error message for pure code	2021-12-13 11:08:38 -08:00
799.lean	fix: generate an error if declaration name clashes with variable name	2022-01-10 12:08:11 -08:00
799.lean.expected.out	fix: generate an error if declaration name clashes with variable name	2022-01-10 12:08:11 -08:00
801.lean	test: wrong test	2022-02-02 13:17:30 +01:00
801.lean.expected.out	test: forgot to commit test for #801	2022-02-02 13:08:23 +01:00
813.lean	fix: remove @[reducible] annotation from Function.comp and Function.const	2021-11-23 07:29:25 -08:00
813.lean.expected.out	fix: remove @[reducible] annotation from Function.comp and Function.const	2021-11-23 07:29:25 -08:00
815b.lean	fix: typo at hasUnusedArguments	2021-12-14 06:50:34 -08:00
815b.lean.expected.out	chore: fix tests	2022-05-31 18:01:48 -07:00
906.lean	fix: increase the number of heartbeats at Expr.eqv	2022-01-26 08:25:33 -08:00
906.lean.expected.out	chore: fix tests	2022-05-31 18:01:48 -07:00
916.lean	test: for #916	2022-01-03 07:57:16 -08:00
916.lean.expected.out	test: for #916	2022-01-03 07:57:16 -08:00
948.lean	fix: ignore TC failures while processing patterns	2022-01-13 10:55:09 -08:00
948.lean.expected.out	fix: use consistent goal prefix everywhere	2022-05-09 17:49:00 +02:00
951.lean	test: add test for issue #951	2022-01-20 17:16:06 -08:00
951.lean.expected.out	test: add test for issue #951	2022-01-20 17:16:06 -08:00
973.lean	feat: generate error message for simp theorems that are equivalent to x = x	2022-01-26 11:16:31 -08:00
973.lean.expected.out	feat: generate error message for simp theorems that are equivalent to x = x	2022-01-26 11:16:31 -08:00
973b.lean	chore: fix tests	2022-06-14 16:43:22 -07:00
973b.lean.expected.out	fix: remove check from Simp.synthesizeArgs	2022-06-03 07:40:30 -07:00
974.lean	test: add variant of Formula.count_quantifiers	2022-01-25 18:47:03 -08:00
974.lean.expected.out	fix: mkEquationsFor at Match/MatchEqs.lean	2022-01-25 18:43:51 -08:00
986.lean	fix: remove irrelevant hypotheses in auto-generated equation theorems	2022-02-02 15:39:51 -08:00
986.lean.expected.out	fix: mkEqnTypes	2022-03-25 19:13:21 -07:00
995.lean	fix: match tactic should not trigger implicit lambdas	2022-02-04 07:55:56 -08:00
995.lean.expected.out	fix: match tactic should not trigger implicit lambdas	2022-02-04 07:55:56 -08:00
1007.lean	feat: improve error message when max heartbeats is reached during TC	2022-02-07 11:23:48 -08:00
1007.lean.expected.out	chore: fix tests	2022-05-31 18:01:48 -07:00
1011.lean	chore: simplify option names	2022-02-08 12:23:24 -08:00
1011.lean.expected.out	feat: relax auto-implicit restrictions	2022-02-08 12:17:42 -08:00
1018unknowMVarIssue.lean	fix: backtrack InfoTree when backtracking at the discriminant refinement method	2022-02-15 16:01:09 -08:00
1018unknowMVarIssue.lean.expected.out	fix: info at pattern variables	2022-05-17 06:28:59 -07:00
1021.lean	fix: nasty bug at findDeclarationRangesCore?	2022-03-19 16:53:22 -07:00
1021.lean.expected.out	chore: use let/if in do blocks	2022-06-13 17:10:14 -07:00
1026.lean	fix: heuristic for generating equation theorem types	2022-02-23 13:10:30 -08:00
1026.lean.expected.out	chore: fix tests	2022-05-31 18:01:48 -07:00
1027.lean	fix: simp_all was "self-simplifying" simplified hypotheses	2022-02-23 16:48:28 -08:00
1027.lean.expected.out	chore: fix tests	2022-05-31 18:01:48 -07:00
1038.lean	fix: toName function at elabAppFnId	2022-03-04 16:56:02 -08:00
1038.lean.expected.out	fix: toName function at elabAppFnId	2022-03-04 16:56:02 -08:00
1039.lean	fix: propagate local and scope modifiers at elab_rules	2022-03-19 16:08:06 -07:00
1039.lean.expected.out	fix: propagate local and scope modifiers at elab_rules	2022-03-19 16:08:06 -07:00
1050.lean	feat: improve "result types must be in the same universe level" error message	2022-03-17 07:41:37 -07:00
1050.lean.expected.out	chore: fix tests	2022-05-31 18:01:48 -07:00
1057.lean	fix: check type mismatch at dependent pattern matching compiler	2022-03-21 09:28:02 -07:00
1057.lean.expected.out	fix: check type mismatch at dependent pattern matching compiler	2022-03-21 09:28:02 -07:00
1062.lean	test: for issue #1062	2022-03-22 14:14:28 -07:00
1062.lean.expected.out	test: for issue #1062	2022-03-22 14:14:28 -07:00
1074a.lean	fix: mkEqnTypes	2022-03-25 19:13:21 -07:00
1074a.lean.expected.out	feat: improve let-pattern and have-pattern macro expansion	2022-03-29 07:33:22 -07:00
1074b.lean	fix: missing test at has_trivial_structure	2022-03-25 17:36:30 -07:00
1074b.lean.expected.out	chore: fix tests	2022-05-31 18:17:56 -07:00
1079.lean	test: for issue #1079	2022-03-28 07:19:55 -07:00
1079.lean.expected.out	test: for issue #1079	2022-03-28 07:19:55 -07:00
1081.lean	fix: smart unfolding	2022-03-29 15:49:14 -07:00
1081.lean.expected.out	fix: smart unfolding	2022-03-29 15:49:14 -07:00
1098.lean	fix: constructor elaboration	2022-04-08 18:19:06 -07:00
1098.lean.expected.out	fix: constructor elaboration	2022-04-08 18:19:06 -07:00
1112.lean	fix: index out of bounds at computeFixedIndexBitMask	2022-04-19 05:21:43 -07:00
1112.lean.expected.out	fix: index out of bounds at computeFixedIndexBitMask	2022-04-19 05:21:43 -07:00
1113.lean	feat: apply rfl theorems at dsimp	2022-04-21 16:26:57 -07:00
1113.lean.expected.out	feat: apply rfl theorems at dsimp	2022-04-21 16:26:57 -07:00
1163.lean	fix: generate sorry warning only if there are no error messages	2022-06-01 06:32:05 -07:00
1163.lean.expected.out	chore: fix tests	2022-06-01 06:36:25 -07:00
1206.lean	fix: check types at do pattern reassignment	2022-06-10 17:31:36 +02:00
1206.lean.expected.out	fix: check types at do pattern reassignment	2022-06-10 17:31:36 +02:00
1235.lean	fix: remove kabstractWithPred	2022-06-20 16:35:18 -07:00
1235.lean.expected.out	fix: remove kabstractWithPred	2022-06-20 16:35:18 -07:00
1240.lean	fix: fixes #1240	2022-06-23 05:53:06 -07:00
1240.lean.expected.out	fix: fixes #1240	2022-06-23 05:53:06 -07:00
abst.lean	chore: fix tests	2021-09-07 19:14:30 -07:00
abst.lean.expected.out
ambiguousOpenExport.lean	feat: report error on ambiguous export and open commands	2022-06-17 09:58:36 -07:00
ambiguousOpenExport.lean.expected.out	feat: report error on ambiguous export and open commands	2022-06-17 09:58:36 -07:00
antiquotRecovery.lean	fix: skip antiquotations during parser recovery	2022-04-27 10:41:27 +02:00
antiquotRecovery.lean.expected.out	fix: skip antiquotations during parser recovery	2022-04-27 10:41:27 +02:00
appParserIssue.lean	refactor: remove optional leading pipe from match, use many1Indent instead of sepBy1	2020-12-16 18:27:05 +01:00
appParserIssue.lean.expected.out	chore: patch tests for pp.analyze default	2021-08-03 09:13:18 +02:00
argNameAtPlaceholderError.lean	feat: show argument name at "don't know how to synthesize placeholder" error messages	2021-12-09 06:48:06 -08:00
argNameAtPlaceholderError.lean.expected.out	fix: tests and add WellFoundedRelation.rel to list of definitions to unfold at decreasing_tactic	2022-01-12 08:28:03 -08:00
argNameIfMacroScopes.lean	feat: show argument name at "don't know how to synthesize placeholder" error messages	2021-12-09 06:48:06 -08:00
argNameIfMacroScopes.lean.expected.out	feat: show argument name at "don't know how to synthesize placeholder" error messages	2021-12-09 06:48:06 -08:00
arrayGetU.lean	feat: add removeUnnecessaryCasts	2022-02-07 17:24:32 -08:00
arrayGetU.lean.expected.out	feat: add removeUnnecessaryCasts	2022-02-07 17:24:32 -08:00
attrCmd.lean
attrCmd.lean.expected.out	test: use printMessageEndPos for leantests	2021-01-15 16:27:59 +01:00
autobound_and_macroscopes.lean	feat: notation: unfold to prechecked quotation	2021-04-27 16:38:37 -07:00
autobound_and_macroscopes.lean.expected.out	chore: fix tests	2022-05-31 18:01:48 -07:00
autoBoundErrorMsg.lean	test: add test for former weird error message	2021-03-23 18:16:06 -07:00
autoBoundErrorMsg.lean.expected.out	feat: improve auto implicit binder names in definitions/theorems	2022-04-07 14:46:59 -07:00
autoBoundImplicits1.lean	chore: simplify option names	2022-02-08 12:23:24 -08:00
autoBoundImplicits1.lean.expected.out	chore: fix tests	2022-06-01 06:36:25 -07:00
autoBoundImplicits2.lean	chore: simplify option names	2022-02-08 12:23:24 -08:00
autoBoundImplicits2.lean.expected.out	feat: pp.analyze original mvars are not unknown	2021-08-03 09:13:18 +02:00
autoBoundPostponeLoop.lean	fix: nontermination	2021-03-18 14:23:03 -07:00
autoBoundPostponeLoop.lean.expected.out	feat: auto local implicit chaining	2022-03-05 17:30:15 -08:00
autoImplicitChain.lean	feat: auto local implicit chaining	2022-03-05 17:30:15 -08:00
autoImplicitChain.lean.expected.out	feat: improve auto implicit binder names in definitions/theorems	2022-04-07 14:46:59 -07:00
autoImplicitChainNameIssue.lean	feat: improve auto implicit binder names in definitions/theorems	2022-04-07 14:46:59 -07:00
autoImplicitChainNameIssue.lean.expected.out	feat: improve auto implicit binder names in definitions/theorems	2022-04-07 14:46:59 -07:00
autoImplicitCtorParamIssue.lean	fix: auto implicit behavior on constructors	2022-05-04 15:04:49 -07:00
autoImplicitCtorParamIssue.lean.expected.out	fix: auto implicit behavior on constructors	2022-05-04 15:04:49 -07:00
autoImplicitForbidden.lean	feat: refine auto bound implicit feature	2022-04-21 10:17:15 -07:00
autoImplicitForbidden.lean.expected.out	feat: refine auto bound implicit feature	2022-04-21 10:17:15 -07:00
autoIssue.lean	feat: improve let-pattern and have-pattern macro expansion	2022-03-29 07:33:22 -07:00
autoIssue.lean.expected.out	feat: improve let-pattern and have-pattern macro expansion	2022-03-29 07:33:22 -07:00
autoPPExplicit.lean	feat: improve application type mismatch error message	2020-12-09 13:58:08 -08:00
autoPPExplicit.lean.expected.out	feat: improve argument type mismatch error position, and do not stop at application type mismatch errors	2022-04-25 16:30:40 -07:00
auxDeclIssue.lean	feat: improve error handling in tactic blocks	2021-05-15 20:18:48 -07:00
auxDeclIssue.lean.expected.out	chore: fix tests	2022-02-23 16:30:27 -08:00
badBinderName.lean	feat: ensure binder names are atomic	2021-01-28 11:27:28 -08:00
badBinderName.lean.expected.out	feat: ensure binder names are atomic	2021-01-28 11:27:28 -08:00
badIhName.lean	refactor: use Lean version	2021-05-03 10:06:20 -07:00
badIhName.lean.expected.out	feat: remove space before propositions with inaccessible names	2022-04-07 07:54:50 -07:00
beginEndAsMacro.lean	feat: revise macro parameter syntax	2021-08-12 07:48:42 -07:00
beginEndAsMacro.lean.expected.out	chore: fix tests	2021-05-17 15:09:51 -07:00
bigUnivOffsets.lean	chore: remove command universes	2021-06-29 17:01:07 -07:00
bigUnivOffsets.lean.expected.out	feat: add option maxUniverseOffset	2021-02-04 17:17:51 -08:00
binderCacheIssue.lean	chore: remove command universes	2021-06-29 17:01:07 -07:00
binderCacheIssue.lean.expected.out	chore: disable pp.analyze for now	2021-09-07 07:51:43 -07:00
binderCacheIssue2.lean	fix: take binder information into account when caching results	2021-05-03 21:02:23 -07:00
binderCacheIssue2.lean.expected.out	chore: disable pp.analyze for now	2021-09-07 07:51:43 -07:00
bindersAbstractingUnassignedMVars.lean	feat: allow mkLambdaFVars and mkForallFVars to abstract unassigned metavars too	2022-03-09 11:27:58 -08:00
bindersAbstractingUnassignedMVars.lean.expected.out	feat: allow mkLambdaFVars and mkForallFVars to abstract unassigned metavars too	2022-03-09 11:27:58 -08:00
binomialHeap.lean	chore: add test case for BinomialHeap	2021-08-17 10:19:12 -07:00
binomialHeap.lean.expected.out	chore: add test case for BinomialHeap	2021-08-17 10:19:12 -07:00
binop_lazy.lean	test: use <|> at binop_lazy test	2021-09-07 17:10:36 -07:00
binop_lazy.lean.expected.out	feat: elaborate binop_lazy%	2021-09-07 13:30:09 -07:00
binopIssues.lean	feat: new elaborator for binop%	2021-08-13 15:44:59 -07:00
binopIssues.lean.expected.out	feat: new elaborator for binop%	2021-08-13 15:44:59 -07:00
binrel_binop.lean	feat: improve binrel% elaborator	2022-05-09 18:39:52 -07:00
binrel_binop.lean.expected.out	chore: fix tests	2022-05-31 18:01:48 -07:00
binsearch.lean	refactor: heterogeneous operators	2020-12-01 14:02:46 -08:00
binsearch.lean.expected.out
bintreeGoal.lean	feat: do not display inaccessible proposition names if they do not have forward dependencies	2022-04-02 13:15:17 -07:00
bintreeGoal.lean.expected.out	chore: fix tests	2022-06-01 06:36:25 -07:00
bitwise.lean	fix: bitwise shift overflow of UInt types	2021-03-17 10:08:02 +01:00
bitwise.lean.expected.out	fix: bitwise shift overflow of UInt types	2021-03-17 10:08:02 +01:00
byCasesMetaM.lean	feat: add Meta.byCases helper tactic	2021-08-16 14:58:51 -07:00
byCasesMetaM.lean.expected.out	feat: add Meta.byCases helper tactic	2021-08-16 14:58:51 -07:00
bytearray.lean	feat: add UInt64 unpackings	2021-07-24 10:45:28 +02:00
bytearray.lean.expected.out	feat: add UInt64 unpackings	2021-07-24 10:45:28 +02:00
cacheIssue.lean	fix: bug at decAux?	2021-09-20 07:12:57 -07:00
cacheIssue.lean.expected.out	chore: disable pp.analyze for now	2021-09-07 07:51:43 -07:00
calcErrors.lean	chore: style use · instead of . for lambda dot notation	2022-03-11 07:49:03 -08:00
calcErrors.lean.expected.out	chore: add type to error message	2021-08-31 10:06:22 -07:00
cdotAtSimpArg.lean	chore: fix tests	2021-09-16 10:29:38 -07:00
cdotAtSimpArg.lean.expected.out	feat: allow cdot notation at simp	2021-04-09 19:50:42 -07:00
cdotTuple.lean	chore: style use · instead of . for lambda dot notation	2022-03-11 07:49:03 -08:00
cdotTuple.lean.expected.out	feat: cdot notation for tuples	2020-12-28 18:08:23 -08:00
class_def_must_fail.lean	chore: remove remaining #lang lean4 in tests	2021-01-27 14:45:31 +01:00
class_def_must_fail.lean.expected.out	feat: allow constants to be type classes	2022-03-20 08:03:34 -07:00
classBadOutParam.lean
classBadOutParam.lean.expected.out	test: use printMessageEndPos for leantests	2021-01-15 16:27:59 +01:00
collectDepsIssue.lean	feat: subsume variables under variable	2021-01-22 14:36:05 +01:00
collectDepsIssue.lean.expected.out	chore: fix tests	2022-05-31 18:01:48 -07:00
commandPrefix.lean	feat: in pure code, do use assume Id monad at do notation	2021-12-10 12:55:14 -08:00
commandPrefix.lean.expected.out	feat: in pure code, do use assume Id monad at do notation	2021-12-10 12:55:14 -08:00
congrThmIssue.lean	test: add test for issue fixed in previous commit	2022-03-14 14:11:08 -07:00
congrThmIssue.lean.expected.out	fix: regression reported at issue #1113	2022-04-23 15:39:04 -07:00
constDelab.lean	fix: Delaborator for constants	2021-03-12 19:51:27 -08:00
constDelab.lean.expected.out	fix: Delaborator for constants	2021-03-12 19:51:27 -08:00
constructorTac.lean	feat: add constructor tactic	2021-05-06 10:40:56 -07:00
constructorTac.lean.expected.out	feat: add constructor tactic	2021-05-06 10:40:56 -07:00
consumePPHint.lean	chore: fix tests	2022-06-14 16:43:22 -07:00
consumePPHint.lean.expected.out	chore: fix tests	2022-05-31 18:01:48 -07:00
conv1.lean	feat: allow conv mode's arg command to access implicit arguments	2022-06-14 16:15:38 -07:00
conv1.lean.expected.out	feat: allow conv mode's arg command to access implicit arguments	2022-06-14 16:15:38 -07:00
convInConv.lean	feat: conv in conv	2021-10-22 13:53:56 -07:00
convInConv.lean.expected.out	chore: fix tests	2022-05-31 18:01:48 -07:00
convPatternAtLetIssue.lean	fix: simpLet	2021-10-22 16:29:00 -07:00
convPatternAtLetIssue.lean.expected.out	fix: use consistent goal prefix everywhere	2022-05-09 17:49:00 +02:00
convPatternMatchIssue.lean	fix: pattern should only match if the head symbols are equal	2021-10-22 14:26:11 -07:00
convPatternMatchIssue.lean.expected.out	fix: use consistent goal prefix everywhere	2022-05-09 17:49:00 +02:00
convZetaLetExt.lean	feat: allow ext conv tactic to go inside let-declarations	2022-06-22 19:27:04 -07:00
convZetaLetExt.lean.expected.out	feat: allow ext conv tactic to go inside let-declarations	2022-06-22 19:27:04 -07:00
copy-produced	chore: fix copy-produced	2021-12-17 12:22:53 +01:00
csimpAttr.lean	feat: apply csimp attribute constant replacements	2021-08-21 12:22:15 -07:00
csimpAttr.lean.expected.out	feat: apply csimp attribute constant replacements	2021-08-21 12:22:15 -07:00
csimpAttrAppend.lean	feat: use simple List.append definition and add csimp theorem	2021-08-21 16:11:54 -07:00
csimpAttrAppend.lean.expected.out	feat: use simple List.append definition and add csimp theorem	2021-08-21 16:11:54 -07:00
ctor_layout.lean
ctor_layout.lean.expected.out	feat: store ModuleData of imported modules in EnvironmentHeader	2022-01-15 10:40:52 -08:00
ctorUnivTooBig.lean	feat: better binder names at reorderCtorArgs	2022-04-03 10:03:47 -07:00
ctorUnivTooBig.lean.expected.out	feat: ignore {} annotation at constructors	2022-04-13 08:30:21 -07:00
dbgMacros.lean	chore: fix tests	2021-03-11 11:35:51 -08:00
dbgMacros.lean.expected.out	chore: fix tests	2021-03-11 11:35:51 -08:00
decimals.lean	chore: add more decimals tests	2021-10-26 11:51:30 -07:00
decimals.lean.expected.out	refactor: reimplement ofScientific for floats	2021-10-26 11:51:30 -07:00
decreasing_by.lean	feat: apply termination tactic provided by user	2021-10-03 18:47:52 -07:00
decreasing_by.lean.expected.out	feat: apply termination tactic provided by user	2021-10-03 18:47:52 -07:00
defaultInstance.lean
defaultInstance.lean.expected.out	chore: improve error message	2021-02-05 12:26:39 -08:00
defaultInstanceWithPrio.lean	fix: fixes #787	2021-11-15 18:31:57 -08:00
defaultInstanceWithPrio.lean.expected.out	fix: fixes #787	2021-11-15 18:31:57 -08:00
defInst.lean	feat: improve #eval command	2022-03-12 19:55:15 -08:00
defInst.lean.expected.out	chore: fix tests	2022-05-31 18:17:56 -07:00
delabUnexpand.lean	feat: top-down heuristic delaboration	2021-08-03 09:13:18 +02:00
delabUnexpand.lean.expected.out	feat: top-down heuristic delaboration	2021-08-03 09:13:18 +02:00
delta.lean	chore: fix tests	2021-09-16 10:29:38 -07:00
delta.lean.expected.out	feat: add delta tactic	2021-09-09 13:07:33 -07:00
derivingDecidableEq.lean	feat: support proofs in deriving DecidableEq	2022-05-30 07:36:30 -07:00
derivingDecidableEq.lean.expected.out	feat: support proofs in deriving DecidableEq	2022-05-30 07:36:30 -07:00
derivingRepr.lean	test: use decide and nativeDecide	2021-03-11 07:46:33 -08:00
derivingRepr.lean.expected.out	fix: fix deriving Repr for structure-like inductives	2021-02-25 13:38:33 -08:00
diamond1.lean	chore: style use · instead of . for lambda dot notation	2022-03-11 07:49:03 -08:00
diamond1.lean.expected.out	feat: print number of parameters for an inductive type	2022-03-08 17:48:46 -08:00
diamond2.lean	chore: style use · instead of . for lambda dot notation	2022-03-11 07:49:03 -08:00
diamond2.lean.expected.out	chore: fix tests	2022-02-14 12:06:03 -08:00
diamond3.lean	chore: style use · instead of . for lambda dot notation	2022-03-11 07:49:03 -08:00
diamond3.lean.expected.out	chore: fix tests	2022-02-14 12:06:03 -08:00
diamond4.lean	fix: binder annotation for class diamond coercions	2021-08-10 06:59:28 -07:00
diamond4.lean.expected.out	fix: binder annotation for class diamond coercions	2021-08-10 06:59:28 -07:00
diamond5.lean	fix: generation of to* field names	2021-08-11 17:25:02 -07:00
diamond5.lean.expected.out	fix: correctly pretty-print @Eq	2022-01-12 09:41:41 +01:00
diamond6.lean	test: copyNewFieldsFrom	2021-08-10 09:19:27 -07:00
diamond6.lean.expected.out	test: copyNewFieldsFrom	2021-08-10 09:19:27 -07:00
diamond7.lean	test: add classes up to Field	2021-08-11 08:51:49 -07:00
diamond7.lean.expected.out	fix: correctly pretty-print @Eq	2022-01-12 09:41:41 +01:00
diamond8.lean	fix: recursively copy subfields in diamond extends	2022-01-29 08:31:34 -08:00
diamond8.lean.expected.out	feat: print number of parameters for an inductive type	2022-03-08 17:48:46 -08:00
diamond9.lean	fix: dependent fields in diamond extensions	2022-02-03 09:17:14 -08:00
diamond9.lean.expected.out	fix: dependent fields in diamond extensions	2022-02-03 09:17:14 -08:00
diamond10.lean	fix: refs to copied subobjects in diamond extension	2022-02-07 10:54:32 -08:00
diamond10.lean.expected.out	fix: refs to copied subobjects in diamond extension	2022-02-07 10:54:32 -08:00
docStr.lean	chore: modify findDocString?	2021-09-21 17:29:40 -07:00
docStr.lean.expected.out	chore: fix test	2022-01-17 17:24:09 -08:00
doErrorMsg.lean	fix: check types at do pattern reassignment	2022-06-10 17:31:36 +02:00
doErrorMsg.lean.expected.out	fix: check types at do pattern reassignment	2022-06-10 17:31:36 +02:00
doIfLet.lean	feat: in pure code, do use assume Id monad at do notation	2021-12-10 12:55:14 -08:00
doIfLet.lean.expected.out	feat: if let pat ← ...	2020-12-20 23:58:29 +01:00
doIssue.lean	chore: remove tryPureCoe?	2022-02-03 16:25:24 -08:00
doIssue.lean.expected.out	feat: improve argument type mismatch error position, and do not stop at application type mismatch errors	2022-04-25 16:30:40 -07:00
doLetLoop.lean	fix: ensure ill-formed if do-statements do not trigger non termination	2021-04-13 15:51:20 -07:00
doLetLoop.lean.expected.out	chore: fix tests	2022-06-01 06:36:25 -07:00
doNotation1.lean	feat: in pure code, do use assume Id monad at do notation	2021-12-10 12:55:14 -08:00
doNotation1.lean.expected.out	chore: fix tests	2021-12-14 09:33:52 +01:00
doSeqRightIssue.lean	chore: simplify option names	2022-02-08 12:23:24 -08:00
doSeqRightIssue.lean.expected.out	chore: fix tests	2022-06-01 06:36:25 -07:00
eagerCoeExpansion.lean	feat: eager coe expansion	2021-02-14 11:34:08 -08:00
eagerCoeExpansion.lean.expected.out	feat: add a proper BEq instance for Nat	2022-03-01 09:01:08 -08:00
eagerUnfoldingIssue.lean	feat: implement MonadLog at CoreM	2022-05-31 17:40:55 -07:00
eagerUnfoldingIssue.lean.expected.out	feat: implement MonadLog at CoreM	2022-05-31 17:40:55 -07:00
elseifDoErrorPos.lean	fix: position information at expandDoIf?	2020-12-26 08:26:54 -08:00
elseifDoErrorPos.lean.expected.out	feat: improve argument type mismatch error position, and do not stop at application type mismatch errors	2022-04-25 16:30:40 -07:00
emptyc.lean
emptyc.lean.expected.out	feat: include types in the "ambiguous, possible interpretations" error message	2022-03-06 07:26:31 -08:00
eoi.lean	chore: improve EOI error message	2021-04-03 11:56:26 +02:00
eoi.lean.expected.out	feat: hide elaboration errors from partial syntax trees by default	2021-04-13 19:24:35 +02:00
eqValue.lean	fix: mkEquationsFor at Match/MatchEqs.lean	2022-01-25 18:43:51 -08:00
eqValue.lean.expected.out	fix: splitMatch tactic	2022-02-02 15:06:03 -08:00
eraseInsts.lean	feat: allow instances to be (temporarily) erased	2021-08-31 15:30:29 -07:00
eraseInsts.lean.expected.out	feat: allow instances to be (temporarily) erased	2021-08-31 15:30:29 -07:00
eraseSimp.lean	feat: simp [-decl]	2021-03-04 17:50:44 -08:00
eraseSimp.lean.expected.out	feat: allow user to "erase" [simp] lemmas	2021-03-04 11:36:12 -08:00
errorOnInductionForNested.lean	feat: generate error message when induction tactic is used on a nested inductive type without specifying an eliminator	2022-03-11 14:45:57 -08:00
errorOnInductionForNested.lean.expected.out	feat: generate error message when induction tactic is used on a nested inductive type without specifying an eliminator	2022-03-11 14:45:57 -08:00
errorRecoveryBug.lean	fix: antipattern	2021-04-07 10:26:05 -07:00
errorRecoveryBug.lean.expected.out	fix: antipattern	2021-04-07 10:26:05 -07:00
eta.lean	feat: add Expr.eta	2021-04-09 14:21:21 -07:00
eta.lean.expected.out	chore: patch tests for pp.analyze default	2021-08-03 09:13:18 +02:00
etaStructIssue.lean	fix: the eta for structures implementation in the elaborator was different from the implementation in the kernel	2022-03-25 18:24:15 -07:00
etaStructIssue.lean.expected.out	fix: the eta for structures implementation in the elaborator was different from the implementation in the kernel	2022-03-25 18:24:15 -07:00
eval_except.lean
eval_except.lean.expected.out	test: use printMessageEndPos for leantests	2021-01-15 16:27:59 +01:00
evalInstMessage.lean	feat: improve error message produced by #eval command when it fails to synthesize "eval" instance	2021-11-05 15:03:57 -07:00
evalInstMessage.lean.expected.out	feat: improve error message produced by #eval command when it fails to synthesize "eval" instance	2021-11-05 15:03:57 -07:00
evalSorry.lean	fix: do not evaluate code containing sorry	2021-01-26 15:01:53 -08:00
evalSorry.lean.expected.out	feat: improve argument type mismatch error position, and do not stop at application type mismatch errors	2022-04-25 16:30:40 -07:00
evalWithMVar.lean
evalWithMVar.lean.expected.out	perf: isClassQuick? was incorrectly producing undef	2022-04-09 10:38:49 -07:00
exactErrorPos.lean	feat: improve error recovery at Tactic.elabTerm	2021-05-06 20:44:36 -07:00
exactErrorPos.lean.expected.out	feat: improve error recovery at Tactic.elabTerm	2021-05-06 20:44:36 -07:00
exitAfterParseError.lean
exitAfterParseError.lean.expected.out	feat: hide elaboration errors from partial syntax trees by default	2021-04-13 19:24:35 +02:00
extract.lean
extract.lean.expected.out
failTac.lean	fix: display all remaining goals at fail tactic error message	2022-02-26 09:49:06 -08:00
failTac.lean.expected.out	fix: display all remaining goals at fail tactic error message	2022-02-26 09:49:06 -08:00
file_not_found.lean	feat: make FilePath a concrete type	2021-05-28 14:19:59 +02:00
file_not_found.lean.expected.out	test: use printMessageEndPos for leantests	2021-01-15 16:27:59 +01:00
filePath.lean	feat: make System.FilePath opaque	2021-05-28 14:19:59 +02:00
filePath.lean.expected.out	feat: make FilePath a concrete type	2021-05-28 14:19:59 +02:00
fixedIndexToParamIssue.lean	feat: implement TODO at "fixed indices to parameters"	2022-04-02 14:37:24 -07:00
fixedIndexToParamIssue.lean.expected.out	feat: better binder names at reorderCtorArgs	2022-04-03 10:03:47 -07:00
fixedIndicesToParams.lean	feat: in an inductive family the longest fixed prefix of indices is now promoted to parameters	2022-03-08 17:56:34 -08:00
fixedIndicesToParams.lean.expected.out	feat: better binder names at reorderCtorArgs	2022-04-03 10:03:47 -07:00
forallMetaBounded.lean	fix: forallMetaTelescope issue	2021-08-06 09:47:10 -07:00
forallMetaBounded.lean.expected.out	fix: forallMetaTelescope issue	2021-08-06 09:47:10 -07:00
forErrors.lean	test: add test for "broken for"	2020-12-25 10:03:42 -08:00
forErrors.lean.expected.out	feat: improve elabMatchAux	2021-01-18 15:33:48 -08:00
Format.lean	chore: remove remaining #lang lean4 in tests	2021-01-27 14:45:31 +01:00
Format.lean.expected.out
funExpected.lean	refactor: heterogeneous operators	2020-12-01 14:02:46 -08:00
funExpected.lean.expected.out	feat: pp.analyze original mvars are not unknown	2021-08-03 09:13:18 +02:00
funInfoBug.lean	fix: typo at ParamInfo.isExplicit	2021-01-11 07:08:17 -08:00
funInfoBug.lean.expected.out	fix: typo at ParamInfo.isExplicit	2021-01-11 07:08:17 -08:00
funParen.lean	fix: fun (x ...) ... should not be treated as a pattern	2022-04-15 10:00:26 -07:00
funParen.lean.expected.out	fix: fun (x ...) ... should not be treated as a pattern	2022-04-15 10:00:26 -07:00
gcd.lean	feat: add Nat.gcd	2021-03-07 18:47:02 -08:00
gcd.lean.expected.out	feat: add Nat.gcd	2021-03-07 18:47:02 -08:00
have.lean	feat: have: remove unnecessary whitespace check and allow name- and type-less have	2021-05-25 14:25:14 +02:00
have.lean.expected.out	feat: have ... := ... syntax closer to let	2021-05-06 15:38:57 -07:00
heapSort.lean	fix: pretty-printing match dependent on let	2022-02-10 10:19:04 +01:00
heapSort.lean.expected.out	chore: fix tests	2022-05-31 18:01:48 -07:00
hidingInaccessibleNames.lean	chore: fix tests	2021-09-16 10:29:38 -07:00
hidingInaccessibleNames.lean.expected.out	feat: improve binder names introduced by the match discriminant refinement feature	2022-04-08 06:49:09 -07:00
holeErrors.lean	feat: produces an error if the declaration body contains a universe parameter that does not occur in the declaration type nor is explicitly provided	2022-06-02 19:43:09 -07:00
holeErrors.lean.expected.out	feat: produces an error if the declaration body contains a universe parameter that does not occur in the declaration type nor is explicitly provided	2022-06-02 19:43:09 -07:00
holes.lean
holes.lean.expected.out	perf: isClassQuick? was incorrectly producing undef	2022-04-09 10:38:49 -07:00
hygienicIntro.lean	feat: add tactic macro unhygienic <tactic-seq>	2021-04-10 16:18:40 -07:00
hygienicIntro.lean.expected.out	feat: improve error recovery at Tactic.elabTerm	2021-05-06 20:44:36 -07:00
implementedByIssue.lean	feat: improve implementedBy errors, and relax type matching test	2022-05-02 08:48:15 -07:00
implementedByIssue.lean.expected.out	feat: improve implementedBy errors, and relax type matching test	2022-05-02 08:48:15 -07:00
implicitLambdaIssue.lean	chore: fixes tests	2021-04-22 20:22:43 -07:00
implicitLambdaIssue.lean.expected.out	test: add Kevin and Yakov's examples	2021-03-25 17:22:14 -07:00
implicitTypePos.lean	fix: position information for implicit type	2021-08-26 08:07:16 -07:00
implicitTypePos.lean.expected.out	feat: add Lean.Elab.Term.getMVarErrorInfo?	2021-12-09 06:48:06 -08:00
inductionErrors.lean	chore: fix tests	2021-08-07 13:22:58 -07:00
inductionErrors.lean.expected.out	chore: fix tests	2022-06-01 06:36:25 -07:00
inductionGen.lean	chore: fix tests	2021-09-16 10:29:38 -07:00
inductionGen.lean.expected.out	chore: fix tests	2022-05-31 18:01:48 -07:00
inductionMutual.lean	feat: better error message for induction tactic on mutually inductives	2021-09-21 06:56:17 -07:00
inductionMutual.lean.expected.out	feat: better error message for induction tactic on mutually inductives	2021-09-21 06:56:17 -07:00
inductive1.lean	chore: remove {} from ctor parser	2022-04-13 08:47:21 -07:00
inductive1.lean.expected.out	feat: allow attributes on structures and inductives	2021-12-23 08:04:36 -08:00
inductiveUnivErrorMsg.lean	feat: improve error message when failing to infer resulting universe level for inductive datatypes and structures	2022-05-10 18:30:53 -07:00
inductiveUnivErrorMsg.lean.expected.out	feat: improve error message when failing to infer resulting universe level for inductive datatypes and structures	2022-05-10 18:30:53 -07:00
infoFromFailure.lean
infoFromFailure.lean.expected.out	feat: improved name-unresolving in delab	2021-09-07 16:26:00 +02:00
infoTree.lean	fix: make info of fields synthesized by structure update synthetic	2022-02-06 08:50:07 -08:00
infoTree.lean.expected.out	feat: turn on info trees by default	2022-05-10 06:24:31 -07:00
inst.lean
inst.lean.expected.out
intModBug.lean	test: test for Int.mod bug	2021-01-31 08:57:41 -08:00
intModBug.lean.expected.out	chore: fix test	2021-02-06 12:54:53 -08:00
intNegSucc.lean	test: for Int.negSucc bug	2021-03-07 13:09:23 -08:00
intNegSucc.lean.expected.out	test: for Int.negSucc bug	2021-03-07 13:09:23 -08:00
introLetBug.lean	fix: intro tactic at let-expr	2022-06-22 16:10:33 -07:00
introLetBug.lean.expected.out	fix: intro tactic at let-expr	2022-06-22 16:10:33 -07:00
invalidFieldName.lean	feat: improve error message	2020-12-22 17:50:26 -08:00
invalidFieldName.lean.expected.out	test: use printMessageEndPos for leantests	2021-01-15 16:27:59 +01:00
invalidInstImplicit.lean	feat: check instance implicit binder annotations	2021-04-28 17:15:08 -07:00
invalidInstImplicit.lean.expected.out	feat: check instance implicit binder annotations	2021-04-28 17:15:08 -07:00
invalidNamedArgs.lean	chore: remove remaining #lang lean4 in tests	2021-01-27 14:45:31 +01:00
invalidNamedArgs.lean.expected.out	chore: remove remaining #lang lean4 in tests	2021-01-27 14:45:31 +01:00
invalidPatternIssue.lean	fix: ensure explicit pattern variables provided by the uses are indeed pattern variables	2022-03-16 07:50:29 -07:00
invalidPatternIssue.lean.expected.out	fix: ensure explicit pattern variables provided by the uses are indeed pattern variables	2022-03-16 07:50:29 -07:00
IRbug.lean
IRbug.lean.expected.out
isDefEqOffsetBug.lean	chore: fix tests	2021-05-04 15:42:03 -07:00
isDefEqOffsetBug.lean.expected.out	feat: include type of type in "mismatch errors"	2021-03-08 09:30:34 -08:00
isNoncomputable.lean	test: for isNoncomputable	2022-02-16 13:37:49 -08:00
isNoncomputable.lean.expected.out	test: for isNoncomputable	2022-02-16 13:37:49 -08:00
jason1.lean	fix: missing error messages	2021-03-05 17:20:04 -08:00
jason1.lean.expected.out	fix: apply after-compilation attributes to inductive/structure decls	2022-05-25 11:32:08 -07:00
jason2.lean	fix: missing error messages	2021-03-05 17:20:04 -08:00
jason2.lean.expected.out	fix: missing error messages	2021-03-05 17:20:04 -08:00
json.lean
json.lean.expected.out	fix: Json.num	2021-02-18 13:27:31 +01:00
kernelMVarBug.lean	fix: missig registerMVarErrorImplicitArgInfo for postponed instance mvars	2021-08-04 16:58:00 -07:00
kernelMVarBug.lean.expected.out	fix: missig registerMVarErrorImplicitArgInfo for postponed instance mvars	2021-08-04 16:58:00 -07:00
keyAttrErase.lean	feat: add support for erasing keyed attributes	2021-09-09 14:28:41 -07:00
keyAttrErase.lean.expected.out	feat: allow ▸ even if the expected type is not available	2022-04-23 08:00:27 -07:00
lazySeq.lean	test: add *> laziness test	2021-09-07 18:03:15 -07:00
lazySeq.lean.expected.out	test: add *> laziness test	2021-09-07 18:03:15 -07:00
LE.lean	chore: remove {} from ctor parser	2022-04-13 08:47:21 -07:00
LE.lean.expected.out	chore: remove {} from ctor parser	2022-04-13 08:47:21 -07:00
lean3RefineBug.lean	test: add test for Lean 3 refine bug reported on Zulip	2022-04-06 16:04:17 -07:00
lean3RefineBug.lean.expected.out	feat: remove space before propositions with inaccessible names	2022-04-07 07:54:50 -07:00
letArrowOutsideDo.lean	feat: improve error message for let ... ← ... outside of a do	2021-12-14 08:56:22 -08:00
letArrowOutsideDo.lean.expected.out	feat: improve error message for let ... ← ... outside of a do	2021-12-14 08:56:22 -08:00
letFun.lean	chore: fix tests	2021-09-16 10:29:38 -07:00
letFun.lean.expected.out	test: add let_fun pretty printing test	2021-09-16 10:14:42 -07:00
letPatIssue.lean	feat: improve let-pattern and have-pattern macro expansion	2022-03-29 07:33:22 -07:00
letPatIssue.lean.expected.out	feat: improve let-pattern and have-pattern macro expansion	2022-03-29 07:33:22 -07:00
letrec1.lean
letrec1.lean.expected.out	fix: binder info range for let rec/where	2022-02-06 07:21:51 -08:00
letrecErrors.lean
letrecErrors.lean.expected.out	fix: binder info range for let rec/where	2022-02-06 07:21:51 -08:00
letRecMissingAnnotation.lean	feat: isolate fixed prefix at well-founded recursion	2022-02-18 10:40:32 -08:00
letRecMissingAnnotation.lean.expected.out	chore: fix tests	2022-03-14 10:05:33 -07:00
liftOverLeft.lean	fix: no method lift over let	2021-04-24 19:33:55 -07:00
liftOverLeft.lean.expected.out	fix: no method lift over let	2021-04-24 19:33:55 -07:00
linterUnusedVariables.lean	fix: ignore hygiened names in unused variables linter	2022-06-18 17:24:08 +02:00
linterUnusedVariables.lean.expected.out	fix: ignore hygiened names in unused variables linter	2022-06-18 17:24:08 +02:00
listLength.lean	feat: use simple List.length definition and add csimp theorem	2021-08-21 13:11:06 -07:00
listLength.lean.expected.out	feat: use simple List.length definition and add csimp theorem	2021-08-21 13:11:06 -07:00
ll_infer_type_bug.lean
ll_infer_type_bug.lean.expected.out	chore: fix tests	2021-12-15 11:42:38 +00:00
localNotationPP.lean	fix: unexpanders should inherit scopedness	2021-03-13 13:20:12 +01:00
localNotationPP.lean.expected.out	fix: unexpanders should inherit scopedness	2021-03-13 13:20:12 +01:00
loopErrorRecovery.lean	fix: loop due to error recovery	2021-04-13 08:12:39 -07:00
loopErrorRecovery.lean.expected.out	fix: loop due to error recovery	2021-04-13 08:12:39 -07:00
lvl1.lean
lvl1.lean.expected.out
macroError.lean	fix: term macro errors should be fatal	2022-01-04 11:20:18 +01:00
macroError.lean.expected.out	fix: term macro errors should be fatal	2022-01-04 11:20:18 +01:00
macroPrio.lean	feat: improve notation for setting parser names and priorities	2020-12-21 09:11:12 -08:00
macroPrio.lean.expected.out	feat: include types in the "ambiguous, possible interpretations" error message	2022-03-06 07:26:31 -08:00
macroResolveName.lean	refactor: resolveNamespace now return a List	2022-06-16 17:16:36 -07:00
macroResolveName.lean.expected.out	refactor: resolveNamespace now return a List	2022-06-16 17:16:36 -07:00
macroscopes.lean	chore: remove when and «unless»	2021-03-20 18:52:18 -07:00
macroscopes.lean.expected.out
macroStack.lean	chore: remove weird syntax sugar from macro command	2020-12-10 08:09:47 -08:00
macroStack.lean.expected.out	feat: improve binrel% elaborator	2022-05-09 18:39:52 -07:00
macroTrace.lean	feat: trace support for MacroM	2021-04-23 19:15:14 -07:00
macroTrace.lean.expected.out	feat: trace support for MacroM	2021-04-23 19:15:14 -07:00
magical.lean	fix: reject projection (_ : ∃ x, p).2	2022-03-01 09:00:46 -08:00
magical.lean.expected.out	fix: reject projection (_ : ∃ x, p).2	2022-03-01 09:00:46 -08:00
mangling.lean	fix: 32-bit Unicode name mangling	2021-06-23 00:08:20 -07:00
mangling.lean.expected.out	fix: make mangling injective again	2021-06-23 00:08:20 -07:00
match1.lean	chore: remove command universes	2021-06-29 17:01:07 -07:00
match1.lean.expected.out	chore: fix tests	2022-02-14 15:47:12 -08:00
match2.lean	feat: ignore {} annotation at constructors	2022-04-13 08:30:21 -07:00
match2.lean.expected.out	chore: fix tests	2022-02-14 15:47:12 -08:00
match3.lean	chore: remove ≅ notation for HEq	2021-09-15 08:06:32 -07:00
match3.lean.expected.out
match4.lean	chore: add simp lemmas, theorem naming convention	2021-02-16 11:53:49 -08:00
match4.lean.expected.out
matchAltIndent.lean	fix: add checkColGe to matchAlt	2021-03-12 11:06:07 -08:00
matchAltIndent.lean.expected.out	fix: add checkColGe to matchAlt	2021-03-12 11:06:07 -08:00
matchApp.lean	feat: top-down heuristic delaboration	2021-08-03 09:13:18 +02:00
matchApp.lean.expected.out	chore: fix tests	2021-12-15 11:42:38 +00:00
matchErrorLocation.lean	feat: (generalizing := true) is the default behavior for match-expressions	2022-02-15 11:12:04 -08:00
matchErrorLocation.lean.expected.out	feat: include type of type in "mismatch errors"	2021-03-08 09:30:34 -08:00
matchErrorMsg.lean	feat: improve match error message	2021-01-14 14:58:34 -08:00
matchErrorMsg.lean.expected.out	fix: no sorry-warning for missing match cases	2022-06-01 07:41:52 -07:00
matchLeftovers.lean	feat: cleanup local context before elaborating match alternatives RHS	2022-03-29 18:52:07 -07:00
matchLeftovers.lean.expected.out	feat: improve binder names introduced by the match discriminant refinement feature	2022-04-08 06:49:09 -07:00
matchMissingCasesAsStuckError.lean	fix: better error message when cases fails and there are no alternatives	2021-03-26 16:28:21 -07:00
matchMissingCasesAsStuckError.lean.expected.out	fix: no sorry-warning for missing match cases	2022-06-01 07:41:52 -07:00
matchMultAlt.lean	feat: macro expand match alternatives	2022-03-20 14:20:13 -07:00
matchMultAlt.lean.expected.out	feat: macro expand match alternatives	2022-03-20 14:20:13 -07:00
matchOfNatIssue.lean	chore: fix tests	2021-09-16 10:29:38 -07:00
matchOfNatIssue.lean.expected.out	feat: convert "orphan" kernel nat literals n into ofNat n	2021-09-08 14:58:13 -07:00
matchOrIssue.lean	fix: match or-pattern	2022-05-25 20:05:46 -07:00
matchOrIssue.lean.expected.out	fix: match or-pattern	2022-05-25 20:05:46 -07:00
matchPatternInsideBinders.lean	fix: make sure we can match pattern inside binders	2021-10-10 15:47:04 -07:00
matchPatternInsideBinders.lean.expected.out	fix: use consistent goal prefix everywhere	2022-05-09 17:49:00 +02:00
matchPatternPartialApp.lean	fix: make sure pattern is tried on partial applications	2021-10-10 15:47:04 -07:00
matchPatternPartialApp.lean.expected.out	fix: use consistent goal prefix everywhere	2022-05-09 17:49:00 +02:00
matchunit.lean	chore: special support for match d with | PUnit.unit => rhs	2021-02-10 09:54:12 -08:00
matchunit.lean.expected.out	feat: add equality proof for named patterns	2022-01-18 12:43:01 -08:00
matchUnknownFVarBug.lean	fix: ensure discriminants are distinct variables	2021-03-26 16:28:21 -07:00
matchUnknownFVarBug.lean.expected.out	fix: no sorry-warning for missing match cases	2022-06-01 07:41:52 -07:00
matchVarNames.lean	feat: improve binder names introduced by the match discriminant refinement feature	2022-04-08 06:49:09 -07:00
matchVarNames.lean.expected.out	feat: improve binder names introduced by the match discriminant refinement feature	2022-04-08 06:49:09 -07:00
metaEvalInstMessage.lean	feat: improve error message produced by #eval command when it fails to synthesize "eval" instance	2021-11-05 15:03:57 -07:00
metaEvalInstMessage.lean.expected.out	feat: improve error message produced by #eval command when it fails to synthesize "eval" instance	2021-11-05 15:03:57 -07:00
missingExplicitWithForwardNamedDep.lean	fix: named argument that depends on missing explicit argument	2020-12-09 16:10:48 -08:00
missingExplicitWithForwardNamedDep.lean.expected.out	chore: disable pp.analyze for now	2021-09-07 07:51:43 -07:00
mkProjStx.lean	feat: add mkProjStx?	2021-08-12 05:41:00 -07:00
mkProjStx.lean.expected.out	feat: add mkProjStx?	2021-08-12 05:41:00 -07:00
modBug.lean	chore: fix tests	2021-08-07 13:22:58 -07:00
modBug.lean.expected.out	feat: improve argument type mismatch error position, and do not stop at application type mismatch errors	2022-04-25 16:30:40 -07:00
moduleDoc.lean	feat: add position to mod doc	2022-02-16 13:50:19 -08:00
moduleDoc.lean.expected.out	test: add test for getModuleDoc?	2021-08-06 14:14:22 -07:00
moduleOf.lean	chore: fix tests	2021-01-11 13:01:04 -08:00
moduleOf.lean.expected.out	test: use printMessageEndPos for leantests	2021-01-15 16:27:59 +01:00
mulcommErrorMessage.lean	feat: improve error message and include variables introduced by the implicit lambda notation	2021-04-24 21:34:42 -07:00
mulcommErrorMessage.lean.expected.out	chore: normalize spelling	2022-05-03 10:26:11 +02:00
multiConstantError.lean	chore: fix tests	2022-06-14 16:43:22 -07:00
multiConstantError.lean.expected.out	chore: fix tests	2022-06-14 17:27:13 -07:00
mutualdef1.lean
mutualdef1.lean.expected.out	test: use printMessageEndPos for leantests	2021-01-15 16:27:59 +01:00
mutualWithNamespaceMacro.lean
mutualWithNamespaceMacro.lean.expected.out	test: use printMessageEndPos for leantests	2021-01-15 16:27:59 +01:00
mutwf1.lean	fix: use PSum instead of Sum when using well-founded recursion	2022-02-17 16:14:34 -08:00
mutwf1.lean.expected.out	chore: fix tests	2022-03-14 10:05:33 -07:00
mvar1.lean	feat: better Repr instances for Level.Data and Expr.Data	2022-01-20 09:45:30 -08:00
mvar1.lean.expected.out	chore: fix tests	2022-03-15 11:35:47 -07:00
mvar2.lean	feat: add Repr instances for Level and Expr	2022-01-20 09:26:06 -08:00
mvar2.lean.expected.out	feat: add Repr instances for Level and Expr	2022-01-20 09:26:06 -08:00
mvar3.lean	refactor: pattern elaboration	2022-03-09 18:19:14 -08:00
mvar3.lean.expected.out	feat: add Repr instances for Level and Expr	2022-01-20 09:26:06 -08:00
mvar_fvar.lean	chore: fix tests	2021-09-07 19:14:30 -07:00
mvar_fvar.lean.expected.out
mvarAtDefaultValue.lean	fix: throw error when default value contains metavariables	2021-02-20 11:31:56 -08:00
mvarAtDefaultValue.lean.expected.out	fix: throw error when default value contains metavariables	2021-02-20 11:31:56 -08:00
nameArgErrorIssue.lean	feat: improve argument type mismatch error position, and do not stop at application type mismatch errors	2022-04-25 16:30:40 -07:00
nameArgErrorIssue.lean.expected.out	chore: fix tests	2022-05-31 18:17:56 -07:00
namedHoles.lean
namedHoles.lean.expected.out	chore: fix tests	2022-05-31 18:17:56 -07:00
namelit.lean	feat: delab Name.mkStr/Num	2021-05-19 09:21:52 +02:00
namelit.lean.expected.out
namePatEqThm.lean	fix: equational lemma generation for definitions using named patterns	2022-01-19 17:45:54 -08:00
namePatEqThm.lean.expected.out	feat: cleanup local context before elaborating match alternatives RHS	2022-03-29 18:52:07 -07:00
nameRepr.lean	fix: Repr Name instance	2021-09-18 15:29:32 -07:00
nameRepr.lean.expected.out	fix: Repr Name instance	2021-09-18 15:29:32 -07:00
negFloat.lean	fix: defaultInstance priorities for Neg Int and OfScientific Float	2021-01-25 13:21:07 -08:00
negFloat.lean.expected.out	fix: defaultInstance priorities for Neg Int and OfScientific Float	2021-01-25 13:21:07 -08:00
newCatPanic.lean	fix: fixes #447	2021-05-08 19:04:12 -07:00
newCatPanic.lean.expected.out	fix: fixes #447	2021-05-08 19:04:12 -07:00
nonAtomicFieldName.lean	fix: ensure field names are atomic	2021-08-09 19:01:08 -07:00
nonAtomicFieldName.lean.expected.out	fix: ensure field names are atomic	2021-08-09 19:01:08 -07:00
noncompSection.lean	feat: add noncomputable sections	2021-12-13 11:02:46 -08:00
noncompSection.lean.expected.out	feat: add noncomputable sections	2021-12-13 11:02:46 -08:00
nondepArrow.lean	fix: non-dependent arrow should not extend local context	2021-06-29 06:31:37 -07:00
nondepArrow.lean.expected.out	fix: non-dependent arrow should not extend local context	2021-06-29 06:31:37 -07:00
nonReserved.lean	chore: remove tryPureCoe?	2022-02-03 16:25:24 -08:00
nonReserved.lean.expected.out
noTabs.lean	test: forgot tabs ban test	2021-04-26 17:09:48 +02:00
noTabs.lean.expected.out	test: forgot tabs ban test	2021-04-26 17:09:48 +02:00
notationDelab.lean	feat: improve the heuristic for notation delab	2022-06-23 13:27:53 -07:00
notationDelab.lean.expected.out	feat: improve the heuristic for notation delab	2022-06-23 13:27:53 -07:00
notationPrecheck.lean	feat: quotation precheck for choice nodes	2022-03-29 10:50:11 +02:00
notationPrecheck.lean.expected.out	feat: quotation precheck for choice nodes	2022-03-29 10:50:11 +02:00
openExport.lean
openExport.lean.expected.out	test: use printMessageEndPos for leantests	2021-01-15 16:27:59 +01:00
openScoped.lean	chore: elaborate open scoped	2021-08-21 07:16:24 -07:00
openScoped.lean.expected.out	fix: correctly pretty-print @Eq	2022-01-12 09:41:41 +01:00
or_shortcircuit.lean	feat: in pure code, do use assume Id monad at do notation	2021-12-10 12:55:14 -08:00
or_shortcircuit.lean.expected.out	fix: adjust code to new match-compiler	2020-12-08 13:46:00 -08:00
parserPrio.lean	chore: two comments about bad pp.analyze behavior	2021-08-03 09:13:18 +02:00
parserPrio.lean.expected.out	feat: include types in the "ambiguous, possible interpretations" error message	2022-03-06 07:26:31 -08:00
partialVariable.lean	fix: panic on variable :	2021-04-23 09:24:35 +02:00
partialVariable.lean.expected.out	feat: add strict implicit binder annotation	2021-08-03 19:10:51 -07:00
patvar.lean	fix: simple-match macro	2021-01-12 06:41:32 -08:00
patvar.lean.expected.out	fix: no sorry-warning for missing match cases	2022-06-01 07:41:52 -07:00
phashmap_inst_coherence.lean	chore: fix test	2021-06-02 10:03:12 -07:00
phashmap_inst_coherence.lean.expected.out	feat: improve argument type mismatch error position, and do not stop at application type mismatch errors	2022-04-25 16:30:40 -07:00
ppExpr.lean	chore: remove unnecessary args	2022-04-07 18:19:15 -07:00
ppExpr.lean.expected.out	fix: bug in ppExpr test	2021-08-03 09:13:18 +02:00
PPInstances.lean	chore: fix tests	2022-06-14 16:43:22 -07:00
PPInstances.lean.expected.out	chore: fix tests	2022-05-31 18:01:48 -07:00
ppite.lean	test: pretty printing if-then-else	2020-12-24 08:40:30 -08:00
ppite.lean.expected.out	fix: use group for if-then-else	2021-12-15 11:42:38 +00:00
pplevel.lean	chore: fix codebase and tests	2021-06-29 17:14:52 -07:00
pplevel.lean.expected.out	fix: correctly pretty-print @Eq	2022-01-12 09:41:41 +01:00
ppMotives.lean	chore: remove ≅ notation for HEq	2021-09-15 08:06:32 -07:00
ppMotives.lean.expected.out	chore: fix tests	2022-02-14 15:47:12 -08:00
ppNotationCode.lean	fix: make precedence mandatory for mixfix commands	2021-07-19 13:18:58 -07:00
ppNotationCode.lean.expected.out	feat: delaborate cond using bif-then-else	2022-03-03 07:41:39 -08:00
ppProofs.lean	feat: pp.analyze isSubstLike support Eq.rec	2021-08-03 09:13:18 +02:00
ppProofs.lean.expected.out	chore: patch tests for pp.analyze default	2021-08-03 09:13:18 +02:00
PPRoundtrip.lean	fix: test	2022-06-17 17:47:51 -07:00
PPRoundtrip.lean.expected.out	feat: define PointedType as { α : Type u // Nonempty α }	2022-01-14 20:36:51 -08:00
ppSyntax.lean
ppSyntax.lean.expected.out
precissues.lean	chore: adapt stdlib & tests	2021-05-20 15:17:36 -07:00
precissues.lean.expected.out	feat: pretty print let_fun	2021-09-11 05:15:11 -07:00
private.lean
private.lean.expected.out	test: use printMessageEndPos for leantests	2021-01-15 16:27:59 +01:00
privateFieldCopyIssue.lean	fix: propagate visibility annotation	2021-08-10 15:34:07 -07:00
privateFieldCopyIssue.lean.expected.out	chore: fix tests	2022-02-14 12:06:03 -08:00
Process.lean	feat: IO.Process.Child.takeStdin	2021-06-11 17:53:51 -07:00
Process.lean.expected.out	feat: IO.Process.Child.takeStdin	2021-06-11 17:53:51 -07:00
protected.lean	feat: subsume variables under variable	2021-01-22 14:36:05 +01:00
protected.lean.expected.out	feat: improve error message produced by #eval command when it fails to synthesize "eval" instance	2021-11-05 15:03:57 -07:00
pureCoeIssue.lean
pureCoeIssue.lean.expected.out	fix: avoid unnecessary unfolding at do	2021-05-02 21:29:32 -07:00
rat1.lean	feat: add Lean.Rat for implementing decision procedures	2021-09-14 19:18:12 -07:00
rat1.lean.expected.out	feat: add Lean.Rat for implementing decision procedures	2021-09-14 19:18:12 -07:00
readDir.lean	feat: make FilePath a concrete type	2021-05-28 14:19:59 +02:00
readDir.lean.expected.out	feat: make System.FilePath opaque	2021-05-28 14:19:59 +02:00
redundantAlt.lean	feat: improve redundant alternative error message	2020-12-29 14:39:45 -08:00
redundantAlt.lean.expected.out	test: use printMessageEndPos for leantests	2021-01-15 16:27:59 +01:00
ref1.lean	feat: force users to use discard when action result is not being bound and it is not PUnit	2020-12-08 06:14:48 -08:00
ref1.lean.expected.out
refineOccursCheck.lean	fix: occurs check at refine tactic	2022-03-31 18:08:05 -07:00
refineOccursCheck.lean.expected.out	fix: occurs check at refine tactic	2022-03-31 18:08:05 -07:00
Reformat.lean	feat: implement MonadLog at CoreM	2022-05-31 17:40:55 -07:00
Reformat.lean.expected.out	chore: fix tests	2022-06-14 17:27:13 -07:00
renameBug.lean	fix: nasty bug at rename tactic	2021-08-25 15:27:29 -07:00
renameBug.lean.expected.out	fix: nasty bug at rename tactic	2021-08-25 15:27:29 -07:00
renameI.lean	chore: fix tests	2021-09-16 10:29:38 -07:00
renameI.lean.expected.out	chore: fix tests	2022-05-31 18:01:48 -07:00
repr.lean	feat: add helper class ReprAtom	2020-12-18 14:14:46 -08:00
repr.lean.expected.out	feat: add helper class ReprAtom	2020-12-18 14:14:46 -08:00
repr_issue.lean
repr_issue.lean.expected.out	chore: fix tests	2020-12-18 11:21:30 -08:00
resolveGlobalName.lean	feat: implement MonadLog at CoreM	2022-05-31 17:40:55 -07:00
resolveGlobalName.lean.expected.out
revertlet.lean	chore: fix tests	2021-09-16 10:29:38 -07:00
revertlet.lean.expected.out	fix: revert	2020-12-31 09:47:05 -08:00
rewrite.lean	chore: fix tests	2021-09-16 10:29:38 -07:00
rewrite.lean.expected.out	feat: remove space before propositions with inaccessible names	2022-04-07 07:54:50 -07:00
rfl_simp_thm.lean	feat: track rfl simp theorems	2022-04-21 13:42:04 -07:00
rfl_simp_thm.lean.expected.out	feat: track rfl simp theorems	2022-04-21 13:42:04 -07:00
root.lean	chore: fix test	2022-06-13 14:06:56 -07:00
root.lean.expected.out	chore: fix test	2022-06-13 14:06:56 -07:00
runSTBug.lean	chore: remove tryPureCoe?	2022-02-03 16:25:24 -08:00
runSTBug.lean.expected.out	fix: bug at runST and runEST	2020-12-06 18:52:28 -08:00
rwEqThms.lean	feat: allow rw to unfold nonrecursive definitions too	2022-03-12 15:44:52 -08:00
rwEqThms.lean.expected.out	chore: fix test	2022-06-07 16:37:45 -07:00
rwWithoutOffsetCnstrs.lean	chore: fix tests	2021-09-16 10:29:38 -07:00
rwWithoutOffsetCnstrs.lean.expected.out	chore: fix tests	2022-05-31 18:01:48 -07:00
safeShadowing.lean	feat: top-down heuristic delaboration	2021-08-03 09:13:18 +02:00
safeShadowing.lean.expected.out	feat: improve binder names introduced by the match discriminant refinement feature	2022-04-08 06:49:09 -07:00
sanitizeMacroScopes.lean
sanitizeMacroScopes.lean.expected.out	chore: patch tests for pp.analyze default	2021-08-03 09:13:18 +02:00
sanitychecks.lean	chore: fix tests	2022-06-14 16:43:22 -07:00
sanitychecks.lean.expected.out	chore: fix tests	2022-06-14 17:27:13 -07:00
scopedInstanceOutsideNamespace.lean	feat: ensure scoped instances cannot be used outside namespaces	2020-12-05 16:26:31 -08:00
scopedInstanceOutsideNamespace.lean.expected.out	feat: copy & store whole ref range in SourceInfo	2021-01-20 16:48:50 +01:00
scopedLocalInsts.lean	test: scoped and local instances	2020-12-05 16:10:27 -08:00
scopedLocalInsts.lean.expected.out	feat: improve error message produced by #eval command when it fails to synthesize "eval" instance	2021-11-05 15:03:57 -07:00
scopedMacros.lean	feat: add scoped macro_rules (#432)	2021-04-30 09:05:09 +02:00
scopedMacros.lean.expected.out	fix: go to definition for macro_rules etc.	2021-11-24 11:54:13 +01:00
scopedTokens.lean	fix: scoped tokens	2020-12-21 13:11:09 -08:00
scopedTokens.lean.expected.out	test: use printMessageEndPos for leantests	2021-01-15 16:27:59 +01:00
scopedunifhint.lean	chore: fix tests	2020-12-28 16:27:38 -08:00
scopedunifhint.lean.expected.out	feat: improve argument type mismatch error position, and do not stop at application type mismatch errors	2022-04-25 16:30:40 -07:00
semicolonOrLinebreak.lean	fix: introduce semicolonOrLinebreak, replace many(1) with sepBy(1) where appropriate	2022-06-16 23:33:57 +02:00
semicolonOrLinebreak.lean.expected.out	fix: introduce semicolonOrLinebreak, replace many(1) with sepBy(1) where appropriate	2022-06-16 23:33:57 +02:00
shadow.lean
shadow.lean.expected.out	fix: add withFreshMacroScope at expandMacroImpl?	2021-10-02 16:57:25 -07:00
simpArgTypeMismatch.lean	chore: fix tests	2021-08-07 13:22:58 -07:00
simpArgTypeMismatch.lean.expected.out	feat: improve argument type mismatch error position, and do not stop at application type mismatch errors	2022-04-25 16:30:40 -07:00
simpcfg.lean	chore: fix tests	2021-09-16 10:29:38 -07:00
simpcfg.lean.expected.out	chore: disable pp.analyze for now	2021-09-07 07:51:43 -07:00
simpDisch.lean	chore: fix tests	2022-06-14 16:43:22 -07:00
simpDisch.lean.expected.out	feat: simp discharger	2021-09-16 10:11:27 -07:00
simpPrefixIssue.lean	chore: fix tests	2021-09-16 10:29:38 -07:00
simpPrefixIssue.lean.expected.out	fix: simp was not applying rewrites to the function application prefixes	2021-09-09 17:07:14 -07:00
simpZetaFalse.lean	chore: fix tests	2022-06-14 16:43:22 -07:00
simpZetaFalse.lean.expected.out	chore: unused variables	2022-06-07 17:54:10 -07:00
sizeof.lean	feat: generate sizeOf equality lemmas for constructors	2021-01-21 17:44:15 -08:00
sizeof.lean.expected.out	fix: correctly pretty-print @Eq	2022-01-12 09:41:41 +01:00
smartUnfolding.lean	chore: fix tests	2021-09-16 10:29:38 -07:00
smartUnfolding.lean.expected.out
smartUnfoldingMatch.lean	chore: fix tests	2022-06-14 16:43:22 -07:00
smartUnfoldingMatch.lean.expected.out	chore: fix tests	2021-12-15 11:42:38 +00:00
sorryAtError.lean	fix: bug at hasSyntheticSorry	2021-03-05 19:08:10 -08:00
sorryAtError.lean.expected.out	feat: improve argument type mismatch error position, and do not stop at application type mismatch errors	2022-04-25 16:30:40 -07:00
sorryWarning.lean	test: sorry warning	2021-01-13 10:30:35 -08:00
sorryWarning.lean.expected.out	chore: fix tests	2022-05-31 18:01:48 -07:00
splitIssue.lean	fix: split tactic issue	2022-04-01 15:47:24 -07:00
splitIssue.lean.expected.out	fix: split tactic issue	2022-04-01 15:47:24 -07:00
stdio.lean
stdio.lean.expected.out
stream.lean	chore: use polymorphic method forIn	2021-02-04 18:13:01 -08:00
stream.lean.expected.out	feat: add helper classes for implementing parallel for	2020-12-19 14:15:47 -08:00
strictImplicit.lean	feat: elaborate strict implicit binders	2021-08-03 19:40:44 -07:00
strictImplicit.lean.expected.out	feat: elaborate strict implicit binders	2021-08-03 19:40:44 -07:00
string_imp.lean
string_imp.lean.expected.out	refactor: make String.Pos opaque	2022-03-20 10:47:13 -07:00
string_imp2.lean	refactor: make String.Pos opaque	2022-03-20 10:47:13 -07:00
string_imp2.lean.expected.out	refactor: make String.Pos opaque	2022-03-20 10:47:13 -07:00
struct1.lean	feat: structure diamonds basic support	2021-08-09 19:01:08 -07:00
struct1.lean.expected.out	chore: modify default value for option structureDiamondWarning	2021-08-10 09:24:53 -07:00
structAutoBound.lean
structAutoBound.lean.expected.out	feat: print number of parameters for an inductive type	2022-03-08 17:48:46 -08:00
structDefault.lean	test: add structure field default value test	2020-12-23 08:35:27 -08:00
structDefault.lean.expected.out	feat: include type of type in "mismatch errors"	2021-03-08 09:30:34 -08:00
structDefValueOverride.lean	feat: process overriden default values in copied parents	2021-08-10 18:55:12 -07:00
structDefValueOverride.lean.expected.out	feat: process overriden default values in copied parents	2021-08-10 18:55:12 -07:00
structInst1.lean	fix: check redundant sources at structure instance notation	2021-08-12 09:16:30 -07:00
structInst1.lean.expected.out	fix: check redundant sources at structure instance notation	2021-08-12 09:16:30 -07:00
structInstError.lean	feat: improve {...} error message	2020-12-24 09:35:55 -08:00
structInstError.lean.expected.out	feat: pp.analyze detect when struct-inst type needed	2021-08-03 09:13:18 +02:00
structSorryBug.lean	chore: simplify option names	2022-02-08 12:23:24 -08:00
structSorryBug.lean.expected.out	feat: relax auto-implicit restrictions	2022-02-08 12:17:42 -08:00
structuralEqns.lean	fix: remove auxiliary discriminant let-declarations	2022-01-07 15:03:19 -08:00
structuralEqns.lean.expected.out	fix: use private names for theorems that are created on demand	2022-02-07 13:16:22 -08:00
StxQuot.lean	feat: $_ antiquotation pattern	2022-06-04 13:57:04 +02:00
StxQuot.lean.expected.out	chore: fix tests	2022-06-16 23:33:57 +02:00
substBadMotive.lean	feat: isolate fixed prefix at well-founded recursion	2022-02-18 10:40:32 -08:00
substBadMotive.lean.expected.out	chore: fix tests	2022-06-01 06:36:25 -07:00
substlet.lean	chore: fix tests	2021-09-16 10:29:38 -07:00
substlet.lean.expected.out	fix: closes #421	2021-04-23 12:27:39 -07:00
syntaxErrors.lean
syntaxErrors.lean.expected.out	test: use printMessageEndPos for leantests	2021-01-15 16:27:59 +01:00
syntaxInNamespacesAndPP.lean	chore: remove tryPureCoe?	2022-02-03 16:25:24 -08:00
syntaxInNamespacesAndPP.lean.expected.out	chore: fix tests	2021-12-15 11:42:38 +00:00
syntaxPrec.lean	chore: align stx precedence in syntax to the new one in macro	2021-08-24 10:11:12 -07:00
syntaxPrec.lean.expected.out	chore: fix test output	2021-09-05 17:49:03 -07:00
syntheticHolesAsPatterns.lean	feat: try to preserve variable names during discriminant refinement	2022-02-15 15:54:03 -08:00
syntheticHolesAsPatterns.lean.expected.out	fix: pattern hover information	2022-04-08 15:03:42 -07:00
tabulate.lean	fix: do not display implicit fields	2022-03-09 12:33:22 -08:00
tabulate.lean.expected.out	fix: do not display implicit fields	2022-03-09 12:33:22 -08:00
tacUnsolvedGoalsErrors.lean	chore: style	2022-03-11 16:12:46 -08:00
tacUnsolvedGoalsErrors.lean.expected.out	feat: remove space before propositions with inaccessible names	2022-04-07 07:54:50 -07:00
tcloop.lean	feat: add options maxHeartbeats and synthInstance.maxHeartbeats	2021-01-24 17:45:50 -08:00
tcloop.lean.expected.out	chore: increase maxHeartbeats default values	2022-02-28 15:44:08 -08:00
termination_by.lean	chore: use termination_by'	2022-01-11 15:00:53 -08:00
termination_by.lean.expected.out	chore: use termination_by'	2022-01-11 15:00:53 -08:00
termination_by2.lean	feat: process termination_by syntax	2022-01-12 16:15:30 -08:00
termination_by2.lean.expected.out	feat: process termination_by syntax	2022-01-12 16:15:30 -08:00
terminationFailure.lean	feat: use sorry instead of trying to synthesize Inhabited at error recovery	2022-02-15 09:15:18 -08:00
terminationFailure.lean.expected.out	feat: add support for guessing (very) simple WF relations	2022-03-02 11:52:00 -08:00
test_single.sh	fix: unused variables linter review comments	2022-06-03 13:03:52 +02:00
theoremType.lean	feat: ensure no unassigned metavariables in the declaration header when type is explicitly provided	2021-01-11 16:40:14 -08:00
theoremType.lean.expected.out	feat: improve error message	2021-03-05 13:42:54 -08:00
thunk.lean	refactor: clean up Thunk	2021-04-22 20:29:08 -07:00
thunk.lean.expected.out	refactor: clean up Thunk	2021-04-22 20:29:08 -07:00
toFieldNameIssue.lean	fix: generation of to* field names	2021-08-11 17:25:02 -07:00
toFieldNameIssue.lean.expected.out	chore: fix tests	2022-02-14 12:06:03 -08:00
tokenErrors.lean	chore: simplify tests	2021-04-05 22:01:56 +02:00
tokenErrors.lean.expected.out	fix: make unterminated comments consume all input	2021-07-22 15:55:12 +02:00
tooManyVarsAtInduction.lean	fix: report error if too many variable names have been provided at induction/cases alternative	2021-03-08 16:26:53 -08:00
tooManyVarsAtInduction.lean.expected.out	chore: fix tests	2022-06-01 06:36:25 -07:00
traceClassScopes.lean	fix: use eraseMacroScopes on trace classes	2021-10-08 11:13:19 -07:00
traceClassScopes.lean.expected.out	fix: use eraseMacroScopes on trace classes	2021-10-08 11:13:19 -07:00
traceStateBactracking.lean	feat: add trace <string> tactic	2022-02-28 11:16:42 -08:00
traceStateBactracking.lean.expected.out	feat: add trace <string> tactic	2022-02-28 11:16:42 -08:00
traceTacticSteps.lean	chore: add test	2021-11-30 15:34:54 +01:00
traceTacticSteps.lean.expected.out	feat: annotate <;> with expected state	2022-04-29 16:16:09 +02:00
treeMap.lean	fix: eta expand partial applications of recursive function being defined	2022-03-14 10:05:33 -07:00
treeMap.lean.expected.out	fix: eta expand partial applications of recursive function being defined	2022-03-14 10:05:33 -07:00
typeIncorrectPat.lean	fix: improve error message at invalid match-expr	2020-12-29 14:21:02 -08:00
typeIncorrectPat.lean.expected.out	feat: include type of type in "mismatch errors"	2021-03-08 09:30:34 -08:00
typeMismatch.lean
typeMismatch.lean.expected.out	feat: include type of type in "mismatch errors"	2021-03-08 09:30:34 -08:00
typeOf.lean	chore: remove old notation	2021-10-02 15:06:40 -07:00
typeOf.lean.expected.out	chore: remove old notation	2021-10-02 15:06:40 -07:00
uintCtors.lean	chore: fix tests	2021-08-07 13:22:58 -07:00
uintCtors.lean.expected.out
uintMatch.lean	fix: pattern matching on UInt	2021-09-05 19:15:59 -07:00
uintMatch.lean.expected.out	fix: pattern matching on UInt	2021-09-05 19:15:59 -07:00
unboxStruct.lean	chore: fix tests	2022-06-14 16:43:22 -07:00
unboxStruct.lean.expected.out	chore: fix test	2021-07-06 17:28:09 +02:00
unexpander.lean	fix: appUnexpander name resolution	2021-10-09 08:29:26 -07:00
unexpander.lean.expected.out	fix: appUnexpander name resolution	2021-10-09 08:29:26 -07:00
unexpandersNamespaces.lean	chore: test unexpanders inside namespaces	2021-08-03 09:13:18 +02:00
unexpandersNamespaces.lean.expected.out	chore: test unexpanders inside namespaces	2021-08-03 09:13:18 +02:00
UnexpandSubtype.lean	feat: unexpander for Subtype	2021-08-12 09:32:33 +02:00
UnexpandSubtype.lean.expected.out	feat: unexpander for Subtype	2021-08-12 09:32:33 +02:00
unfold1.lean	fix: unfold declarations tagged with [matchPattern] at reduceMatcher? even if transparency setting is not the default one	2022-06-06 15:53:40 -07:00
unfold1.lean.expected.out	fix: unfold declarations tagged with [matchPattern] at reduceMatcher? even if transparency setting is not the default one	2022-06-06 15:53:40 -07:00
unfoldDefEq.lean	fix: simp at local declaration should not create an auxiliary declaration when result is definitionally equal	2022-04-11 07:54:15 -07:00
unfoldDefEq.lean.expected.out	chore: fix tests	2022-05-31 18:01:48 -07:00
unfoldFailure.lean	feat: unfold should fail if it didn't unfold anything	2022-05-09 06:41:17 -07:00
unfoldFailure.lean.expected.out	feat: unfold should fail if it didn't unfold anything	2022-05-09 06:41:17 -07:00
unfoldReduceMatch.lean	feat: unfold tactic tries to reduce match after unfolding	2022-05-09 06:35:40 -07:00
unfoldReduceMatch.lean.expected.out	chore: fix tests	2022-05-31 18:01:48 -07:00
unhygienic.lean	feat: option for disabling hygiene	2021-01-29 15:26:06 +01:00
unhygienic.lean.expected.out	chore: patch tests for pp.analyze default	2021-08-03 09:13:18 +02:00
unifHintAndTC.lean	feat: unification hints + type classes	2021-01-11 15:34:57 -08:00
unifHintAndTC.lean.expected.out	feat: better bottom-up/structure-type heuristics	2021-08-03 09:13:18 +02:00
univInference.lean	chore: remove command universes	2021-06-29 17:01:07 -07:00
univInference.lean.expected.out	feat: improve error message when failing to infer resulting universe level for inductive datatypes and structures	2022-05-10 18:30:53 -07:00
unknownId.lean	fix: avoid macro scopes in error message	2020-12-11 11:23:44 -08:00
unknownId.lean.expected.out	test: use printMessageEndPos for leantests	2021-01-15 16:27:59 +01:00
unknownTactic.lean	chore: adapt stdlib & tests	2021-05-20 15:17:36 -07:00
unknownTactic.lean.expected.out	feat: remove space before propositions with inaccessible names	2022-04-07 07:54:50 -07:00
unnecessaryUnfolding.lean
unnecessaryUnfolding.lean.expected.out
unsolvedIndCases.lean	feat: improve generalizing at induction	2021-03-27 14:28:03 -07:00
unsolvedIndCases.lean.expected.out	fix: leftovers in the local context when applying induction	2021-03-27 19:42:22 -07:00
unsound.lean	fix: missing check at infer_proj	2022-02-25 07:15:34 -08:00
unsound.lean.expected.out	feat: check for invalid projections during elaboration	2022-02-25 07:43:37 -08:00
unused_univ.lean	chore: remove command universes	2021-06-29 17:01:07 -07:00
unused_univ.lean.expected.out	test: use printMessageEndPos for leantests	2021-01-15 16:27:59 +01:00
unusedLet.lean	fix: preserve unused let declarations	2021-10-18 17:40:15 -07:00
unusedLet.lean.expected.out	chore: fix tests	2022-02-14 15:47:12 -08:00
wf1.lean	feat: arity mismatch error message at well-founded recursion	2021-09-21 20:34:15 -07:00
wf1.lean.expected.out	feat: add support for guessing (very) simple WF relations	2022-03-02 11:52:00 -08:00
wf2.lean	chore: use termination_by'	2022-01-11 15:00:53 -08:00
wf2.lean.expected.out	feat: remove space before propositions with inaccessible names	2022-04-07 07:54:50 -07:00
wfrecUnusedLet.lean	fix: tests and add WellFoundedRelation.rel to list of definitions to unfold at decreasing_tactic	2022-01-12 08:28:03 -08:00
wfrecUnusedLet.lean.expected.out	chore: unused variables	2022-06-07 17:54:10 -07:00
whnfProj.lean	chore: fix tests	2021-03-10 18:45:22 -08:00
whnfProj.lean.expected.out	fix: unfold class projections when using TransparencyMode.instances	2021-01-25 12:30:26 -08:00
wildcardAlt.lean	chore: ensure _ alternative is the last one in the cases and induction tactics	2022-04-18 11:18:03 -07:00
wildcardAlt.lean.expected.out	chore: ensure _ alternative is the last one in the cases and induction tactics	2022-04-18 11:18:03 -07:00
zipper.lean	chore: fix tests	2022-01-15 12:18:09 -08:00
zipper.lean.expected.out