| .. |
|
interactive
|
chore: fix test
|
2022-03-03 19:53:35 -08:00 |
|
Reformat
|
|
|
|
run
|
feat: allow interpretation of constants initialized by native code
|
2022-03-07 10:59:49 +01:00 |
|
server
|
chore: remove tryPureCoe?
|
2022-02-03 16:25:24 -08:00 |
|
trust0
|
|
|
|
.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
|
|
|
|
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
|
|
|
|
241.lean.expected.out
|
|
|
|
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
|
|
|
|
243.lean.expected.out
|
feat: improved name-unresolving in delab
|
2021-09-07 16:26:00 +02:00 |
|
247.lean
|
|
|
|
247.lean.expected.out
|
|
|
|
248.lean
|
|
|
|
248.lean.expected.out
|
|
|
|
255.lean
|
|
|
|
255.lean.expected.out
|
chore: disable pp.analyze for now
|
2021-09-07 07:51:43 -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
|
|
|
|
277a.lean.expected.out
|
chore: show declaration with sorry in #eval
|
2022-01-17 13:18:22 -08:00 |
|
277b.lean
|
|
|
|
277b.lean.expected.out
|
chore: show declaration with sorry in #eval
|
2022-01-17 13:18:22 -08:00 |
|
283.lean
|
|
|
|
283.lean.expected.out
|
chore: disable pp.analyze for now
|
2021-09-07 07:51:43 -07:00 |
|
297.lean
|
|
|
|
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
|
|
|
|
301.lean.expected.out
|
chore: fix tests
|
2021-12-15 11:42:38 +00:00 |
|
302.lean
|
|
|
|
302.lean.expected.out
|
feat: auto local implicit chaining
|
2022-03-05 17:30:15 -08:00 |
|
307.lean
|
|
|
|
307.lean.expected.out
|
|
|
|
309.lean
|
|
|
|
309.lean.expected.out
|
|
|
|
331.lean
|
|
|
|
331.lean.expected.out
|
|
|
|
343.lean
|
chore: fix tests
|
2021-08-13 17:24:58 -07:00 |
|
343.lean.expected.out
|
feat: pp.analyze original mvars are not unknown
|
2021-08-03 09:13:18 +02:00 |
|
345.lean
|
|
|
|
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
|
|
|
|
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
|
|
|
|
348.lean.expected.out
|
|
|
|
353.lean
|
|
|
|
353.lean.expected.out
|
|
|
|
361.lean
|
chore: fix test
|
2022-01-31 16:45:57 -08:00 |
|
361.lean.expected.out
|
chore: fix test
|
2022-01-31 16:45:57 -08:00 |
|
366.lean
|
|
|
|
366.lean.expected.out
|
fix: correctly pretty-print @Eq
|
2022-01-12 09:41:41 +01:00 |
|
386.lean
|
|
|
|
386.lean.expected.out
|
|
|
|
389.lean
|
|
|
|
389.lean.expected.out
|
feat: pp.analyze original mvars are not unknown
|
2021-08-03 09:13:18 +02:00 |
|
414.lean
|
|
|
|
414.lean.expected.out
|
|
|
|
415.lean
|
|
|
|
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
|
|
|
|
423.lean
|
|
|
|
423.lean.expected.out
|
chore: fix tests
|
2021-08-13 17:24:58 -07:00 |
|
435.lean
|
|
|
|
435.lean.expected.out
|
|
|
|
435b.lean
|
|
|
|
435b.lean.expected.out
|
|
|
|
439.lean
|
fix: correctly pretty-print @Eq
|
2022-01-12 09:41:41 +01:00 |
|
439.lean.expected.out
|
fix: correctly pretty-print @Eq
|
2022-01-12 09:41:41 +01:00 |
|
440.lean
|
|
|
|
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
|
chore: fix tests
|
2021-12-15 11:42:38 +00:00 |
|
448.lean
|
chore: remove tryPureCoe?
|
2022-02-03 16:25:24 -08:00 |
|
448.lean.expected.out
|
|
|
|
449.lean
|
|
|
|
449.lean.expected.out
|
|
|
|
450.lean
|
|
|
|
450.lean.expected.out
|
feat: add Lean.Elab.Term.getMVarErrorInfo?
|
2021-12-09 06:48:06 -08:00 |
|
456.lean
|
|
|
|
456.lean.expected.out
|
|
|
|
469.lean
|
|
|
|
469.lean.expected.out
|
|
|
|
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
|
feat: reject user declared namespaces containing _root
|
2022-01-26 19:15:45 -08:00 |
|
490.lean.expected.out
|
feat: reject user declared namespaces containing _root
|
2022-01-26 19:15:45 -08:00 |
|
496.lean
|
|
|
|
496.lean.expected.out
|
|
|
|
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
|
|
|
|
550.lean.expected.out
|
|
|
|
586.lean
|
|
|
|
586.lean.expected.out
|
|
|
|
593.lean
|
|
|
|
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
|
fix: handle MData-wrapped app fns consistently in delaborator
|
2021-08-11 18:53:32 +02: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
|
fix: trace_state messages should not be lost during backtracking
|
2022-02-28 11:07:41 -08: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
|
fix: typo at hasUnusedArguments
|
2021-12-14 06:50:34 -08: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: increase maxHeartbeats default values
|
2022-02-28 15:44:08 -08: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: ignore TC failures while processing patterns
|
2022-01-13 10:55:09 -08: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
|
feat: do not try to discharge hypotheses at simp when type contains assignable metavariables
|
2022-01-26 17:57:52 -08:00 |
|
973b.lean.expected.out
|
feat: do not try to discharge hypotheses at simp when type contains assignable metavariables
|
2022-01-26 17:57:52 -08: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: remove irrelevant hypotheses in auto-generated equation theorems
|
2022-02-02 15:39:51 -08: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: increase maxHeartbeats default values
|
2022-02-28 15:44:08 -08: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: backtrack InfoTree when backtracking at the discriminant refinement method
|
2022-02-15 16:01:09 -08:00 |
|
1026.lean
|
fix: heuristic for generating equation theorem types
|
2022-02-23 13:10:30 -08:00 |
|
1026.lean.expected.out
|
fix: heuristic for generating equation theorem types
|
2022-02-23 13:10:30 -08:00 |
|
1027.lean
|
fix: simp_all was "self-simplifying" simplified hypotheses
|
2022-02-23 16:48:28 -08:00 |
|
1027.lean.expected.out
|
fix: trace_state messages should not be lost during backtracking
|
2022-02-28 11:07:41 -08: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 |
|
abst.lean
|
chore: fix tests
|
2021-09-07 19:14:30 -07:00 |
|
abst.lean.expected.out
|
|
|
|
appParserIssue.lean
|
|
|
|
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
|
|
|
|
autobound_and_macroscopes.lean
|
|
|
|
autobound_and_macroscopes.lean.expected.out
|
|
|
|
autoBoundErrorMsg.lean
|
|
|
|
autoBoundErrorMsg.lean.expected.out
|
feat: auto local implicit chaining
|
2022-03-05 17:30:15 -08:00 |
|
autoBoundImplicits1.lean
|
chore: simplify option names
|
2022-02-08 12:23:24 -08:00 |
|
autoBoundImplicits1.lean.expected.out
|
fix: correctly pretty-print @Eq
|
2022-01-12 09:41:41 +01: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
|
|
|
|
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: auto local implicit chaining
|
2022-03-05 17:30:15 -08:00 |
|
autoPPExplicit.lean
|
|
|
|
autoPPExplicit.lean.expected.out
|
feat: pp.analyze original mvars are not unknown
|
2021-08-03 09:13:18 +02:00 |
|
auxDeclIssue.lean
|
|
|
|
auxDeclIssue.lean.expected.out
|
chore: fix tests
|
2022-02-23 16:30:27 -08:00 |
|
badBinderName.lean
|
|
|
|
badBinderName.lean.expected.out
|
|
|
|
badIhName.lean
|
|
|
|
badIhName.lean.expected.out
|
|
|
|
beginEndAsMacro.lean
|
feat: revise macro parameter syntax
|
2021-08-12 07:48:42 -07:00 |
|
beginEndAsMacro.lean.expected.out
|
|
|
|
bigUnivOffsets.lean
|
|
|
|
bigUnivOffsets.lean.expected.out
|
|
|
|
binderCacheIssue.lean
|
|
|
|
binderCacheIssue.lean.expected.out
|
chore: disable pp.analyze for now
|
2021-09-07 07:51:43 -07:00 |
|
binderCacheIssue2.lean
|
|
|
|
binderCacheIssue2.lean.expected.out
|
chore: disable pp.analyze for now
|
2021-09-07 07:51:43 -07: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 |
|
binsearch.lean
|
|
|
|
binsearch.lean.expected.out
|
|
|
|
bitwise.lean
|
|
|
|
bitwise.lean.expected.out
|
|
|
|
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
|
|
|
|
bytearray.lean.expected.out
|
|
|
|
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: remove ≅ notation for HEq
|
2021-09-15 08:06:32 -07: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
|
|
|
|
cdotTuple.lean
|
|
|
|
cdotTuple.lean.expected.out
|
|
|
|
class_def_must_fail.lean
|
|
|
|
class_def_must_fail.lean.expected.out
|
|
|
|
classBadOutParam.lean
|
|
|
|
classBadOutParam.lean.expected.out
|
|
|
|
collectDepsIssue.lean
|
|
|
|
collectDepsIssue.lean.expected.out
|
|
|
|
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 |
|
constDelab.lean
|
|
|
|
constDelab.lean.expected.out
|
|
|
|
constructorTac.lean
|
|
|
|
constructorTac.lean.expected.out
|
|
|
|
consumePPHint.lean
|
fix: do not consume pretty print hints at isDefEq
|
2021-10-20 15:58:56 -07:00 |
|
consumePPHint.lean.expected.out
|
fix: trace_state messages should not be lost during backtracking
|
2022-02-28 11:07:41 -08:00 |
|
conv1.lean
|
chore: fix tests
|
2021-09-16 10:29:38 -07:00 |
|
conv1.lean.expected.out
|
feat: change lhs and rhs conv tactic semantics
|
2021-09-05 09:29:40 -07:00 |
|
convInConv.lean
|
feat: conv in conv
|
2021-10-22 13:53:56 -07:00 |
|
convInConv.lean.expected.out
|
fix: trace_state messages should not be lost during backtracking
|
2022-02-28 11:07:41 -08:00 |
|
convPatternAtLetIssue.lean
|
fix: simpLet
|
2021-10-22 16:29:00 -07:00 |
|
convPatternAtLetIssue.lean.expected.out
|
fix: simpLet
|
2021-10-22 16:29:00 -07: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: pattern should only match if the head symbols are equal
|
2021-10-22 14:26:11 -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 |
|
dbgMacros.lean
|
|
|
|
dbgMacros.lean.expected.out
|
|
|
|
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
|
|
|
|
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: add support for classes with a prefix of outParams at deriving ...
|
2021-09-03 11:33:09 -07:00 |
|
defInst.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 |
|
delabUnexpand.lean
|
|
|
|
delabUnexpand.lean.expected.out
|
|
|
|
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 |
|
derivingRepr.lean
|
|
|
|
derivingRepr.lean.expected.out
|
|
|
|
diamond1.lean
|
feat: structure diamonds basic support
|
2021-08-09 19:01:08 -07:00 |
|
diamond1.lean.expected.out
|
feat: structure diamonds basic support
|
2021-08-09 19:01:08 -07:00 |
|
diamond2.lean
|
feat: add coercion to parent structure whose fields having been copied
|
2021-08-09 19:01:08 -07:00 |
|
diamond2.lean.expected.out
|
chore: fix tests
|
2022-02-14 12:06:03 -08:00 |
|
diamond3.lean
|
test: structure diamond coercion
|
2021-08-10 06:31:44 -07: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
|
fix: recursively copy subfields in diamond extends
|
2022-01-29 08:31:34 -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
|
|
|
|
doErrorMsg.lean.expected.out
|
chore: fix tests
|
2021-12-14 09:33:52 +01: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
|
|
|
|
doIssue.lean
|
chore: remove tryPureCoe?
|
2022-02-03 16:25:24 -08:00 |
|
doIssue.lean.expected.out
|
|
|
|
doLetLoop.lean
|
|
|
|
doLetLoop.lean.expected.out
|
|
|
|
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
|
|
|
|
eagerCoeExpansion.lean
|
|
|
|
eagerCoeExpansion.lean.expected.out
|
feat: add a proper BEq instance for Nat
|
2022-03-01 09:01:08 -08:00 |
|
eagerUnfoldingIssue.lean
|
|
|
|
eagerUnfoldingIssue.lean.expected.out
|
|
|
|
elseifDoErrorPos.lean
|
|
|
|
elseifDoErrorPos.lean.expected.out
|
fix: correctly pretty-print @Eq
|
2022-01-12 09:41:41 +01: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
|
|
|
|
eoi.lean.expected.out
|
|
|
|
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
|
|
|
|
eraseSimp.lean.expected.out
|
|
|
|
errorRecoveryBug.lean
|
|
|
|
errorRecoveryBug.lean.expected.out
|
|
|
|
eta.lean
|
|
|
|
eta.lean.expected.out
|
chore: patch tests for pp.analyze default
|
2021-08-03 09:13:18 +02:00 |
|
eval_except.lean
|
|
|
|
eval_except.lean.expected.out
|
|
|
|
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
|
|
|
|
evalSorry.lean.expected.out
|
chore: show declaration with sorry in #eval
|
2022-01-17 13:18:22 -08:00 |
|
evalWithMVar.lean
|
|
|
|
evalWithMVar.lean.expected.out
|
chore: remove problematic instance hasOfNatOfCoe
|
2022-01-20 14:47:25 -08:00 |
|
exactErrorPos.lean
|
|
|
|
exactErrorPos.lean.expected.out
|
|
|
|
exitAfterParseError.lean
|
|
|
|
exitAfterParseError.lean.expected.out
|
|
|
|
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
|
|
|
|
file_not_found.lean.expected.out
|
|
|
|
filePath.lean
|
|
|
|
filePath.lean.expected.out
|
|
|
|
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
|
|
|
|
forErrors.lean.expected.out
|
|
|
|
Format.lean
|
|
|
|
Format.lean.expected.out
|
|
|
|
funExpected.lean
|
|
|
|
funExpected.lean.expected.out
|
feat: pp.analyze original mvars are not unknown
|
2021-08-03 09:13:18 +02:00 |
|
funInfoBug.lean
|
|
|
|
funInfoBug.lean.expected.out
|
|
|
|
gcd.lean
|
|
|
|
gcd.lean.expected.out
|
|
|
|
have.lean
|
|
|
|
have.lean.expected.out
|
|
|
|
heapSort.lean
|
fix: pretty-printing match dependent on let
|
2022-02-10 10:19:04 +01:00 |
|
heapSort.lean.expected.out
|
fix: pretty-printing match dependent on let
|
2022-02-10 10:19:04 +01:00 |
|
hidingInaccessibleNames.lean
|
chore: fix tests
|
2021-09-16 10:29:38 -07:00 |
|
hidingInaccessibleNames.lean.expected.out
|
chore: disable pp.analyze for now
|
2021-09-07 07:51:43 -07:00 |
|
holeErrors.lean
|
|
|
|
holeErrors.lean.expected.out
|
chore: fix tests
|
2022-01-10 14:33:02 -08:00 |
|
holes.lean
|
|
|
|
holes.lean.expected.out
|
chore: fix tests
|
2022-02-09 10:13:52 -08:00 |
|
hygienicIntro.lean
|
|
|
|
hygienicIntro.lean.expected.out
|
|
|
|
implicitLambdaIssue.lean
|
|
|
|
implicitLambdaIssue.lean.expected.out
|
|
|
|
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
|
|
|
|
inductionGen.lean
|
chore: fix tests
|
2021-09-16 10:29:38 -07:00 |
|
inductionGen.lean.expected.out
|
fix: trace_state messages should not be lost during backtracking
|
2022-02-28 11:07:41 -08: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
|
feat: allow attributes on structures and inductives
|
2021-12-23 08:04:36 -08:00 |
|
inductive1.lean.expected.out
|
feat: allow attributes on structures and inductives
|
2021-12-23 08:04:36 -08: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
|
chore: fix tests
|
2022-02-09 10:13:52 -08:00 |
|
inst.lean
|
|
|
|
inst.lean.expected.out
|
|
|
|
intModBug.lean
|
|
|
|
intModBug.lean.expected.out
|
|
|
|
intNegSucc.lean
|
|
|
|
intNegSucc.lean.expected.out
|
|
|
|
invalidFieldName.lean
|
|
|
|
invalidFieldName.lean.expected.out
|
|
|
|
invalidInstImplicit.lean
|
|
|
|
invalidInstImplicit.lean.expected.out
|
|
|
|
invalidNamedArgs.lean
|
|
|
|
invalidNamedArgs.lean.expected.out
|
|
|
|
IRbug.lean
|
|
|
|
IRbug.lean.expected.out
|
|
|
|
isDefEqOffsetBug.lean
|
|
|
|
isDefEqOffsetBug.lean.expected.out
|
|
|
|
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
|
|
|
|
jason1.lean.expected.out
|
chore: fix tests
|
2022-02-09 10:13:52 -08:00 |
|
jason2.lean
|
|
|
|
jason2.lean.expected.out
|
|
|
|
json.lean
|
|
|
|
json.lean.expected.out
|
|
|
|
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: add support for erasing keyed attributes
|
2021-09-09 14:28:41 -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 |
|
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 |
|
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: clarify error message at decreasing_tactic
|
2022-02-26 10:15:05 -08:00 |
|
liftOverLeft.lean
|
|
|
|
liftOverLeft.lean.expected.out
|
|
|
|
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
|
|
|
|
localNotationPP.lean.expected.out
|
|
|
|
loopErrorRecovery.lean
|
|
|
|
loopErrorRecovery.lean.expected.out
|
|
|
|
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
|
|
|
|
macroPrio.lean.expected.out
|
feat: include types in the "ambiguous, possible interpretations" error message
|
2022-03-06 07:26:31 -08:00 |
|
macroResolveName.lean
|
|
|
|
macroResolveName.lean.expected.out
|
feat: pp.analyze original mvars are not unknown
|
2021-08-03 09:13:18 +02:00 |
|
macroscopes.lean
|
|
|
|
macroscopes.lean.expected.out
|
|
|
|
macroStack.lean
|
|
|
|
macroStack.lean.expected.out
|
chore: fix tests
|
2021-08-13 17:24:58 -07:00 |
|
macroTrace.lean
|
|
|
|
macroTrace.lean.expected.out
|
|
|
|
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
|
|
|
|
mangling.lean.expected.out
|
|
|
|
match1.lean
|
|
|
|
match1.lean.expected.out
|
chore: fix tests
|
2022-02-14 15:47:12 -08:00 |
|
match2.lean
|
chore: fix tests
|
2022-02-14 15:47:12 -08: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
|
|
|
|
match4.lean.expected.out
|
|
|
|
matchAltIndent.lean
|
|
|
|
matchAltIndent.lean.expected.out
|
|
|
|
matchApp.lean
|
|
|
|
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
|
|
|
|
matchErrorMsg.lean
|
|
|
|
matchErrorMsg.lean.expected.out
|
|
|
|
matchMissingCasesAsStuckError.lean
|
|
|
|
matchMissingCasesAsStuckError.lean.expected.out
|
|
|
|
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 |
|
matchPatternInsideBinders.lean
|
fix: make sure we can match pattern inside binders
|
2021-10-10 15:47:04 -07:00 |
|
matchPatternInsideBinders.lean.expected.out
|
fix: make sure we can match pattern inside binders
|
2021-10-10 15:47:04 -07: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: make sure pattern is tried on partial applications
|
2021-10-10 15:47:04 -07:00 |
|
matchunit.lean
|
|
|
|
matchunit.lean.expected.out
|
feat: add equality proof for named patterns
|
2022-01-18 12:43:01 -08:00 |
|
matchUnknownFVarBug.lean
|
|
|
|
matchUnknownFVarBug.lean.expected.out
|
|
|
|
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
|
|
|
|
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
|
chore: disable pp.analyze for now
|
2021-09-07 07:51:43 -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
|
|
|
|
moduleOf.lean.expected.out
|
|
|
|
mulcommErrorMessage.lean
|
|
|
|
mulcommErrorMessage.lean.expected.out
|
chore: disable pp.analyze for now
|
2021-09-07 07:51:43 -07:00 |
|
multiConstantError.lean
|
feat: improve error message for constant a b c : Nat
|
2021-08-26 08:26:33 -07:00 |
|
multiConstantError.lean.expected.out
|
feat: add Lean.Elab.Term.getMVarErrorInfo?
|
2021-12-09 06:48:06 -08:00 |
|
mutualdef1.lean
|
|
|
|
mutualdef1.lean.expected.out
|
|
|
|
mutualWithNamespaceMacro.lean
|
|
|
|
mutualWithNamespaceMacro.lean.expected.out
|
|
|
|
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: clarify error message at decreasing_tactic
|
2022-02-26 10:15:05 -08: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
|
feat: better Repr instances for Level.Data and Expr.Data
|
2022-01-20 09:45:30 -08: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
|
feat: add Repr instances for Level and Expr
|
2022-01-20 09:26:06 -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
|
|
|
|
mvarAtDefaultValue.lean.expected.out
|
|
|
|
namedHoles.lean
|
|
|
|
namedHoles.lean.expected.out
|
chore: disable pp.analyze for now
|
2021-09-07 07:51:43 -07:00 |
|
namelit.lean
|
|
|
|
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
|
fix: splitMatch tactic
|
2022-02-02 15:06:03 -08: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
|
|
|
|
negFloat.lean.expected.out
|
|
|
|
newCatPanic.lean
|
|
|
|
newCatPanic.lean.expected.out
|
|
|
|
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
|
|
|
|
nondepArrow.lean.expected.out
|
|
|
|
nonReserved.lean
|
chore: remove tryPureCoe?
|
2022-02-03 16:25:24 -08:00 |
|
nonReserved.lean.expected.out
|
|
|
|
noTabs.lean
|
|
|
|
noTabs.lean.expected.out
|
|
|
|
notationPrecheck.lean
|
|
|
|
notationPrecheck.lean.expected.out
|
|
|
|
openExport.lean
|
|
|
|
openExport.lean.expected.out
|
|
|
|
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
|
|
|
|
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
|
|
|
|
partialVariable.lean.expected.out
|
feat: add strict implicit binder annotation
|
2021-08-03 19:10:51 -07:00 |
|
patvar.lean
|
|
|
|
patvar.lean.expected.out
|
|
|
|
phashmap_inst_coherence.lean
|
|
|
|
phashmap_inst_coherence.lean.expected.out
|
feat: add a proper BEq instance for Nat
|
2022-03-01 09:01:08 -08:00 |
|
ppExpr.lean
|
fix: bug in ppExpr test
|
2021-08-03 09:13:18 +02:00 |
|
ppExpr.lean.expected.out
|
fix: bug in ppExpr test
|
2021-08-03 09:13:18 +02:00 |
|
PPInstances.lean
|
feat: pp.instances and pp.instanceTypes
|
2021-08-12 09:33:30 +02:00 |
|
PPInstances.lean.expected.out
|
feat: pp.instances and pp.instanceTypes
|
2021-08-12 09:33:30 +02:00 |
|
ppite.lean
|
|
|
|
ppite.lean.expected.out
|
fix: use group for if-then-else
|
2021-12-15 11:42:38 +00:00 |
|
pplevel.lean
|
|
|
|
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
|
|
|
|
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
|
feat: define PointedType as { α : Type u // Nonempty α }
|
2022-01-14 20:36:51 -08: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
|
|
|
|
precissues.lean.expected.out
|
feat: pretty print let_fun
|
2021-09-11 05:15:11 -07:00 |
|
private.lean
|
|
|
|
private.lean.expected.out
|
|
|
|
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
|
|
|
|
Process.lean.expected.out
|
|
|
|
protected.lean
|
|
|
|
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
|
|
|
|
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
|
|
|
|
readDir.lean.expected.out
|
|
|
|
redundantAlt.lean
|
|
|
|
redundantAlt.lean.expected.out
|
|
|
|
ref1.lean
|
|
|
|
ref1.lean.expected.out
|
|
|
|
Reformat.lean
|
chore: fix tests
|
2021-08-06 14:05:00 -07:00 |
|
Reformat.lean.expected.out
|
chore: fix tests
|
2021-12-15 11:42:38 +00: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
|
fix: trace_state messages should not be lost during backtracking
|
2022-02-28 11:07:41 -08:00 |
|
repr.lean
|
|
|
|
repr.lean.expected.out
|
|
|
|
repr_issue.lean
|
|
|
|
repr_issue.lean.expected.out
|
|
|
|
resolveGlobalName.lean
|
|
|
|
resolveGlobalName.lean.expected.out
|
|
|
|
revertlet.lean
|
chore: fix tests
|
2021-09-16 10:29:38 -07:00 |
|
revertlet.lean.expected.out
|
|
|
|
rewrite.lean
|
chore: fix tests
|
2021-09-16 10:29:38 -07:00 |
|
rewrite.lean.expected.out
|
feat: pp.analyze original mvars are not unknown
|
2021-08-03 09:13:18 +02:00 |
|
runSTBug.lean
|
chore: remove tryPureCoe?
|
2022-02-03 16:25:24 -08:00 |
|
runSTBug.lean.expected.out
|
|
|
|
rwWithoutOffsetCnstrs.lean
|
chore: fix tests
|
2021-09-16 10:29:38 -07:00 |
|
rwWithoutOffsetCnstrs.lean.expected.out
|
fix: trace_state messages should not be lost during backtracking
|
2022-02-28 11:07:41 -08:00 |
|
safeShadowing.lean
|
|
|
|
safeShadowing.lean.expected.out
|
chore: fix tests
|
2021-12-15 11:42:38 +00:00 |
|
sanitizeMacroScopes.lean
|
|
|
|
sanitizeMacroScopes.lean.expected.out
|
chore: patch tests for pp.analyze default
|
2021-08-03 09:13:18 +02:00 |
|
sanitychecks.lean
|
feat: when Lean cannot prove termination, then report error and add definition as partial, and if it fails add as axiom
|
2022-02-15 07:44:27 -08:00 |
|
sanitychecks.lean.expected.out
|
feat: make sure packDomain and packMutual ignore the fixed arguments
|
2022-02-17 17:43:06 -08:00 |
|
scopedInstanceOutsideNamespace.lean
|
|
|
|
scopedInstanceOutsideNamespace.lean.expected.out
|
|
|
|
scopedLocalInsts.lean
|
|
|
|
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
|
|
|
|
scopedMacros.lean.expected.out
|
fix: go to definition for macro_rules etc.
|
2021-11-24 11:54:13 +01:00 |
|
scopedTokens.lean
|
|
|
|
scopedTokens.lean.expected.out
|
|
|
|
scopedunifhint.lean
|
|
|
|
scopedunifhint.lean.expected.out
|
feat: pp.analyze original mvars are not unknown
|
2021-08-03 09:13:18 +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
|
chore: fix tests
|
2021-08-07 13:22:58 -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
|
2021-09-16 10:29:38 -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
|
2021-09-16 10:29:38 -07:00 |
|
simpZetaFalse.lean.expected.out
|
feat: basic support for linear Nat arithmetic at simp
|
2022-02-26 08:58:32 -08:00 |
|
sizeof.lean
|
|
|
|
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
|
fix: to do unfold matcher applications that cannot be reduced when smartUnfolding is true
|
2021-08-17 21:32:32 -07:00 |
|
smartUnfoldingMatch.lean.expected.out
|
chore: fix tests
|
2021-12-15 11:42:38 +00:00 |
|
sorryAtError.lean
|
|
|
|
sorryAtError.lean.expected.out
|
|
|
|
sorryWarning.lean
|
|
|
|
sorryWarning.lean.expected.out
|
|
|
|
stdio.lean
|
|
|
|
stdio.lean.expected.out
|
|
|
|
stream.lean
|
|
|
|
stream.lean.expected.out
|
|
|
|
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
|
|
|
|
string_imp2.lean
|
|
|
|
string_imp2.lean.expected.out
|
|
|
|
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
|
|
|
|
structDefault.lean
|
|
|
|
structDefault.lean.expected.out
|
|
|
|
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
|
|
|
|
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
|
chore: remove tryPureCoe?
|
2022-02-03 16:25:24 -08:00 |
|
StxQuot.lean.expected.out
|
chore: fix tests
|
2022-02-14 15:47:12 -08:00 |
|
substBadMotive.lean
|
feat: isolate fixed prefix at well-founded recursion
|
2022-02-18 10:40:32 -08:00 |
|
substBadMotive.lean.expected.out
|
fix: check generated motives at ▸ notation
|
2021-12-15 16:16:42 -08:00 |
|
substlet.lean
|
chore: fix tests
|
2021-09-16 10:29:38 -07:00 |
|
substlet.lean.expected.out
|
|
|
|
syntaxErrors.lean
|
|
|
|
syntaxErrors.lean.expected.out
|
|
|
|
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
|
feat: try to preserve variable names during discriminant refinement
|
2022-02-15 15:54:03 -08:00 |
|
tacUnsolvedGoalsErrors.lean
|
|
|
|
tacUnsolvedGoalsErrors.lean.expected.out
|
|
|
|
tcloop.lean
|
|
|
|
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
|
|
|
|
theoremType.lean
|
|
|
|
theoremType.lean.expected.out
|
|
|
|
thunk.lean
|
|
|
|
thunk.lean.expected.out
|
|
|
|
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
|
|
|
|
tokenErrors.lean.expected.out
|
|
|
|
tooManyVarsAtInduction.lean
|
|
|
|
tooManyVarsAtInduction.lean.expected.out
|
|
|
|
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
|
chore: fix tests
|
2021-12-15 11:42:38 +00:00 |
|
typeIncorrectPat.lean
|
|
|
|
typeIncorrectPat.lean.expected.out
|
|
|
|
typeMismatch.lean
|
|
|
|
typeMismatch.lean.expected.out
|
|
|
|
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
|
|
|
|
unboxStruct.lean.expected.out
|
|
|
|
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: use PSum instead of Sum when using well-founded recursion
|
2022-02-17 16:14:34 -08:00 |
|
unfold1.lean.expected.out
|
test: unfold tactic
|
2022-01-07 13:51:45 -08:00 |
|
unhygienic.lean
|
|
|
|
unhygienic.lean.expected.out
|
chore: patch tests for pp.analyze default
|
2021-08-03 09:13:18 +02:00 |
|
unifHintAndTC.lean
|
|
|
|
unifHintAndTC.lean.expected.out
|
feat: better bottom-up/structure-type heuristics
|
2021-08-03 09:13:18 +02:00 |
|
univInference.lean
|
|
|
|
univInference.lean.expected.out
|
|
|
|
unknownId.lean
|
|
|
|
unknownId.lean.expected.out
|
|
|
|
unknownTactic.lean
|
|
|
|
unknownTactic.lean.expected.out
|
|
|
|
unnecessaryUnfolding.lean
|
|
|
|
unnecessaryUnfolding.lean.expected.out
|
|
|
|
unsolvedIndCases.lean
|
|
|
|
unsolvedIndCases.lean.expected.out
|
|
|
|
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
|
|
|
|
unused_univ.lean.expected.out
|
|
|
|
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
|
chore: clarify error message at decreasing_tactic
|
2022-02-26 10:15:05 -08: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
|
fix: use group for if-then-else
|
2021-12-15 11:42:38 +00:00 |
|
whnfProj.lean
|
|
|
|
whnfProj.lean.expected.out
|
|
|
|
zipper.lean
|
chore: fix tests
|
2022-01-15 12:18:09 -08:00 |
|
zipper.lean.expected.out
|
|
|
