lean4-htt

History

Leonardo de Moura ee0bcc8321 feat: add `Simp.Config.index` (#4202 ) The `simp` tactic uses a discrimination tree to select candidate theorems that will be used to rewrite an expression. This indexing data structure minimizes the number of theorems that need to be tried and improves performance. However, indexing modulo reducibility is challenging, and a theorem that could be applied, when taking reduction into account, may be missed. For example, suppose we have a `simp` theorem `foo : forall x y, f x (x, y).2 = y`, and we are trying to simplify the expression `f a b <= b`. `foo` will not be tried by `simp` because the second argument of `f a b` is not a projection of a pair. However, `f a b` is definitionally equal to `f a (a, b).2` since we can reduce `(a, b).2`. In Lean 3, we had a much simpler indexing data structure where only the head symbol was taken into account. For the theorem `foo`, the head symbol is `f`. Thus, the theorem would be considered by `simp`. This commit adds the option `Simp.Config.index`. When `simp (config := { index := false })`, only the head symbol is considered when retrieving theorems, as in Lean 3. Moreover, if `set_option diagnostics true`, `simp` will check whether every applied theorem would also have been applied if `index := true`, and report them. This feature can help users diagnose tricky issues in code that has been ported from libraries developed using Lean 3 and then ported to Lean 4. In the following example, it will report that `foo` is a problematic theorem. ```lean opaque f : Nat → Nat → Nat @[simp] theorem foo : f x (x, y).2 = y := by sorry example : f a b ≤ b := by set_option diagnostics true in simp (config := { index := false }) ``` In the example above, the following diagnostic message is produced. ```lean [simp] theorems with bad keys foo, key: [f, , Prod.1, Prod.mk, Nat, Nat, , *] ``` With the information above, users can annotate theorems such as `foo` using `no_index` for problematic subterms. Example: ```lean opaque f : Nat → Nat → Nat @[simp] theorem foo : f x (no_index (x, y).2) = y := by sorry example : f a b ≤ b := by simp -- `foo` is still applied ``` cc @semorrison cc @PatrickMassot		2024-05-17 21:14:58 +00:00
..
interactive	feat: hover / go-to-def for `attribute` cmd (#3896 )	2024-04-13 07:13:25 +00:00
new-compiler	chore: default `compiler.enableNew` to false until development restarts (#3034 )	2023-12-21 07:48:25 +00:00
Reformat	chore: snake-case attributes (part 1)	2022-10-19 09:28:08 -07:00
run	feat: add `Simp.Config.index` (#4202 )	2024-05-17 21:14:58 +00:00
server	feat: snapshot trees and language processors (#3014 )	2024-03-14 13:40:08 +00:00
trust0
.gitignore
217.lean
217.lean.expected.out	chore: fix tests after hash change	2022-12-01 20:18:14 -08:00
220.lean
220.lean.expected.out
223.lean
223.lean.expected.out
236.lean
236.lean.expected.out
241.lean
241.lean.expected.out	fix: more accurate invalid shadowin error position	2022-08-13 18:07:30 -07:00
242.lean
242.lean.expected.out
243.lean
243.lean.expected.out	feat: apply `pp_using_anonymous_constructor` attribute (#3735 )	2024-03-22 00:30:36 +00:00
247.lean
247.lean.expected.out
248.lean	chore: snake-case attributes (part 1)	2022-10-19 09:28:08 -07:00
248.lean.expected.out	chore: snake-case attributes (part 1)	2022-10-19 09:28:08 -07:00
255.lean
255.lean.expected.out
276.lean	chore: upstream Std.Logic (#3312 )	2024-02-14 09:40:55 +00:00
276.lean.expected.out	chore: upstream Std.Logic (#3312 )	2024-02-14 09:40:55 +00:00
277a.lean
277a.lean.expected.out
277b.lean
277b.lean.expected.out
283.lean
283.lean.expected.out	feat: extract `delabAppCore`, define `withOverApp`, and make over-applied projections pretty print (#3083 )	2024-01-10 13:24:28 +00:00
297.lean
297.lean.expected.out	fix: type class issues with `maxSynthPendingDepth := 1` (#4119 )	2024-05-14 03:03:32 +00:00
301.lean
301.lean.expected.out	feat: apply app unexpanders for all prefixes of an application (#3375 )	2024-02-27 07:04:17 +00:00
302.lean
302.lean.expected.out
307.lean
307.lean.expected.out
309.lean
309.lean.expected.out
331.lean	feat: allow optional type in `example`	2022-09-13 03:11:04 -07:00
331.lean.expected.out	feat: allow optional type in `example`	2022-09-13 03:11:04 -07:00
345.lean
345.lean.expected.out	fix: type class issues with `maxSynthPendingDepth := 1` (#4119 )	2024-05-14 03:03:32 +00:00
346.lean
346.lean.expected.out
348.lean
348.lean.expected.out	feat: include unexpected token in error message	2023-09-12 11:42:24 +02:00
353.lean	chore: snake-case attributes (part 1)	2022-10-19 09:28:08 -07:00
353.lean.expected.out
361.lean
361.lean.expected.out	feat: include unexpected token in error message	2023-09-12 11:42:24 +02:00
366.lean
366.lean.expected.out	fix: add missing registerTraceClass `Meta.synthInstance.instances (#4151 )	2024-05-15 18:59:01 +00:00
386.lean
386.lean.expected.out	fix: type class issues with `maxSynthPendingDepth := 1` (#4119 )	2024-05-14 03:03:32 +00:00
389.lean
389.lean.expected.out	refactor: replace `ignoreLevelMVarDepth` by `levelAssignDepth`	2022-12-19 20:14:17 +01:00
414.lean
414.lean.expected.out
415.lean
415.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
421.lean
421.lean.expected.out
423.lean
423.lean.expected.out
435.lean
435.lean.expected.out
435b.lean
435b.lean.expected.out
439.lean	chore: remove unexpanded coercion support from pp.analyze	2022-08-24 21:58:13 -07:00
439.lean.expected.out	feat: add `pp.fieldNotation.generalized` for generalized field notation, add `@[pp_nodot]` attribute (#3737 )	2024-03-22 08:55:02 +00:00
440.lean
440.lean.expected.out	feat: use signature pretty printer in `#check id`/`#check @id`	2022-12-21 21:59:05 +01:00
445.lean	refactor: simplify `runTermElabM` and `liftTermElabM`	2022-08-07 07:35:02 -07:00
445.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
448.lean
448.lean.expected.out	fix: type class issues with `maxSynthPendingDepth := 1` (#4119 )	2024-05-14 03:03:32 +00:00
449.lean
449.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
450.lean
450.lean.expected.out	chore: fix tests	2022-11-30 17:52:37 -08:00
469.lean	feat: apply app unexpanders for all prefixes of an application (#3375 )	2024-02-27 07:04:17 +00:00
469.lean.expected.out	fix: notation delaborator on over-application	2022-07-25 13:42:37 -07:00
474.lean	refactor: add doc strings, cleanup, and dotted notation friendly API	2022-07-27 16:01:15 -07:00
474.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
490.lean
490.lean.expected.out
496.lean
496.lean.expected.out
529.lean
529.lean.expected.out
550.lean
550.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
586.lean
586.lean.expected.out	chore: unexpanders for `Name.mkStr` and `Array.mkArray`	2022-10-04 17:18:36 -07:00
593.lean
593.lean.expected.out	feat: use signature pretty printer in `#check id`/`#check @id`	2022-12-21 21:59:05 +01:00
603.lean
603.lean.expected.out
604.lean
604.lean.expected.out	feat: make `#check <ident>` always show the signature without elaboration	2022-12-21 21:59:05 +01:00
620.lean
620.lean.expected.out
621.lean	feat: shorten auto-generated instance names (#3089 )	2024-04-13 18:08:50 +00:00
621.lean.expected.out	feat: shorten auto-generated instance names (#3089 )	2024-04-13 18:08:50 +00:00
625.lean	chore: snake-case attributes (part 1)	2022-10-19 09:28:08 -07:00
625.lean.expected.out
641.lean
641.lean.expected.out
653.lean
653.lean.expected.out	fix: Format.align always prints whitespace	2022-12-21 22:54:42 +01:00
655.lean
655.lean.expected.out
679.lean
679.lean.expected.out
689.lean
689.lean.expected.out	feat: include unexpected token in error message	2023-09-12 11:42:24 +02:00
690.lean
690.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
697.lean
697.lean.expected.out
714.lean
714.lean.expected.out	fix: make `delabConstWithSignature` avoid using inaccessible names (#3625 )	2024-03-07 18:14:06 +00:00
755.lean
755.lean.expected.out	feat: shorten auto-generated instance names (#3089 )	2024-04-13 18:08:50 +00:00
770.lean
770.lean.expected.out	chore: consistent use of backticks in error messages at `Do.lean`	2022-07-24 07:42:04 -07:00
799.lean
799.lean.expected.out
801.lean
801.lean.expected.out
813.lean
813.lean.expected.out
815b.lean	chore: fix tests	2022-08-15 08:55:25 -07:00
815b.lean.expected.out	fix: add missing registerTraceClass `Meta.synthInstance.instances (#4151 )	2024-05-15 18:59:01 +00:00
906.lean	feat: per-function termination hints	2024-01-10 17:27:35 +01:00
906.lean.expected.out	chore: fix tests	2024-05-01 03:19:39 +02:00
916.lean
916.lean.expected.out	fix: more accurate invalid shadowin error position	2022-08-13 18:07:30 -07:00
948.lean	feat: in conv tactic, use `try with_reducibe rfl` (#3763 )	2024-03-29 11:59:45 +00:00
948.lean.expected.out
951.lean	feat: shorten auto-generated instance names (#3089 )	2024-04-13 18:08:50 +00:00
951.lean.expected.out	feat: shorten auto-generated instance names (#3089 )	2024-04-13 18:08:50 +00:00
973.lean
973.lean.expected.out	feat: ensure projections are not reducing at `DiscrTree V (simpleReduce := true)`	2022-11-15 16:47:12 -08:00
973b.lean	feat: enable failIfUnchanged by default in simp	2023-08-16 10:14:23 -07:00
973b.lean.expected.out	feat: improve `simp` discharge trace messages (#3523 )	2024-02-28 04:39:57 +00:00
995.lean
995.lean.expected.out
1007.lean	feat: reorder tc subgoals according to out-params	2023-04-10 13:00:04 -07:00
1007.lean.expected.out	fix: type class issues with `maxSynthPendingDepth := 1` (#4119 )	2024-05-14 03:03:32 +00:00
1011.lean	feat: allow upper case single character identifiers when relaxedAutoImplicit false (#2277 )	2023-06-19 20:04:09 -07:00
1011.lean.expected.out	feat: allow upper case single character identifiers when relaxedAutoImplicit false (#2277 )	2023-06-19 20:04:09 -07:00
1018unknowMVarIssue.lean
1018unknowMVarIssue.lean.expected.out	fix: don't use info nodes before cursor for completion (#3778 )	2024-04-02 08:49:24 +00:00
1021.lean
1021.lean.expected.out	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
1027.lean
1027.lean.expected.out
1038.lean
1038.lean.expected.out
1039.lean	chore: snake-case attributes (part 1)	2022-10-19 09:28:08 -07:00
1039.lean.expected.out
1050.lean	feat: per-function termination hints	2024-01-10 17:27:35 +01:00
1050.lean.expected.out	feat: per-function termination hints	2024-01-10 17:27:35 +01:00
1057.lean
1057.lean.expected.out
1062.lean
1062.lean.expected.out
1074b.lean
1074b.lean.expected.out	chore: fix tests	2022-10-11 17:24:35 -07:00
1079.lean	chore: fix tests	2022-08-15 08:55:25 -07:00
1079.lean.expected.out	chore: bool and prop lemmas for Mathlib compatibility and improved confluence (#3508 )	2024-03-04 23:56:30 +00:00
1081.lean
1081.lean.expected.out	feat: apply `pp_using_anonymous_constructor` attribute (#3735 )	2024-03-22 00:30:36 +00:00
1098.lean	feat: make `#check <ident>` always show the signature without elaboration	2022-12-21 21:59:05 +01:00
1098.lean.expected.out	feat: use signature pretty printer in `#check id`/`#check @id`	2022-12-21 21:59:05 +01:00
1102.lean	feat: reorder tc subgoals according to out-params	2023-04-10 13:00:04 -07:00
1102.lean.expected.out	fix: type class issues with `maxSynthPendingDepth := 1` (#4119 )	2024-05-14 03:03:32 +00:00
1112.lean
1112.lean.expected.out
1113.lean
1113.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
1163.lean	feat: dynamic quotations for categories	2022-10-18 14:59:14 -07:00
1163.lean.expected.out	fix: type class issues with `maxSynthPendingDepth := 1` (#4119 )	2024-05-14 03:03:32 +00:00
1206.lean	chore: move Std.* data structures to Lean.*	2022-09-26 05:46:04 -07:00
1206.lean.expected.out
1235.lean
1235.lean.expected.out
1240.lean	chore: split up & simplify `importModules`	2023-08-31 15:37:33 -04:00
1240.lean.expected.out	chore: split up & simplify `importModules`	2023-08-31 15:37:33 -04:00
1275.lean	fix: wrap `&"..." <\|> ...` as well	2022-10-28 21:25:47 +02:00
1275.lean.expected.out	fix: Format.align always prints whitespace	2022-12-21 22:54:42 +01:00
1279.lean
1279.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
1279_simplified.lean
1279_simplified.lean.expected.out
1292.lean
1292.lean.expected.out
1298.lean	chore: upstream NatCast and IntCast (#3347 )	2024-02-16 00:54:22 +00:00
1298.lean.expected.out
1301.lean
1301.lean.expected.out	feat: improve `runTactic`	2022-07-25 07:41:50 -07:00
1321.lean
1321.lean.expected.out	chore: unexpanders for `Name.mkStr` and `Array.mkArray`	2022-10-04 17:18:36 -07:00
1358.lean	fix: ensure messages associated with last exception are not lost at `evalTactic`	2022-07-22 12:05:29 -04:00
1358.lean.expected.out	fix: ensure messages associated with last exception are not lost at `evalTactic`	2022-07-22 12:05:29 -04:00
1363.lean	feat: per-function termination hints	2024-01-10 17:27:35 +01:00
1363.lean.expected.out	chore: snake-case attributes (part 1)	2022-10-19 09:28:08 -07:00
1367.lean	fix: notation delaborator on over-application	2022-07-25 13:42:37 -07:00
1367.lean.expected.out	fix: notation delaborator on over-application	2022-07-25 13:42:37 -07:00
1371.lean	fix: unused `match`-syntax alternatives are silently ignored	2022-07-31 06:00:08 -07:00
1371.lean.expected.out	fix: unused `match`-syntax alternatives are silently ignored	2022-07-31 06:00:08 -07:00
1377.lean	fix: preserve user-facing names and `BinderInfo` when lifting `let-rec` declarations	2022-07-28 06:36:45 -07:00
1377.lean.expected.out	fix: make `delabConstWithSignature` avoid using inaccessible names (#3625 )	2024-03-07 18:14:06 +00:00
1433.lean	fix: bug at `lean_nat_mod`	2022-08-06 08:07:25 -07:00
1433.lean.expected.out	fix: bug at `lean_nat_mod`	2022-08-06 08:07:25 -07:00
1569.lean	fix: disable auto implicit feature when running tactics	2022-09-09 15:17:50 -07:00
1569.lean.expected.out	fix: disable auto implicit feature when running tactics	2022-09-09 15:17:50 -07:00
1571.lean	fix: fixes #1571	2022-09-15 11:16:16 -07:00
1571.lean.expected.out	fix: fixes #1571	2022-09-15 11:16:16 -07:00
1576.lean	fix: fixes #1576	2022-09-09 14:29:48 -07:00
1576.lean.expected.out	fix: fixes #1576	2022-09-09 14:29:48 -07:00
1606.lean	feat: use colEq in sepByIndent	2022-09-19 12:44:43 -07:00
1606.lean.expected.out	feat: include unexpected token in error message	2023-09-12 11:42:24 +02:00
1616.lean	fix: stop iterating over visited mvars in `collectUnassignedMVars`	2023-05-15 09:37:19 -07:00
1616.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
1668.lean	fix: derive Repr missing a comma	2022-10-01 07:17:57 -07:00
1668.lean.expected.out	fix: derive Repr missing a comma	2022-10-01 07:17:57 -07:00
1673.lean	fix: fixes #1673	2022-10-02 08:23:14 -07:00
1673.lean.expected.out	fix: Float RecApp out of applications (#2818 )	2023-11-22 14:25:09 +00:00
1681.lean	fix: fixes #1681	2022-10-07 18:36:25 -07:00
1681.lean.expected.out	fix: fixes #1681	2022-10-07 18:36:25 -07:00
1682.lean	feat: sort `refine` new goals using the order they were created	2022-10-04 06:54:14 -07:00
1682.lean.expected.out	feat: sort `refine` new goals using the order they were created	2022-10-04 06:54:14 -07:00
1690.lean	fix: avoid nontermination on non-utf8 input	2022-10-06 17:45:21 -07:00
1690.lean.expected.out	fix: avoid nontermination on non-utf8 input	2022-10-06 17:45:21 -07:00
1705.lean	fix: fixes #1705	2022-10-07 13:11:26 -07:00
1705.lean.expected.out	feat: include unexpected token in error message	2023-09-12 11:42:24 +02:00
1707.lean	fix: fixes #1707	2022-10-08 07:58:56 -07:00
1707.lean.expected.out	feat: include unexpected token in error message	2023-09-12 11:42:24 +02:00
1719.lean	feat: improve `apply` error message when root term elaboration is postponed	2022-10-26 17:15:24 -07:00
1719.lean.expected.out	feat: improve `apply` error message when root term elaboration is postponed	2022-10-26 17:15:24 -07:00
1760.lean	fix: do not create choice nodes for failed parses	2022-11-11 09:13:02 +01:00
1760.lean.expected.out	feat: include unexpected token in error message	2023-09-12 11:42:24 +02:00
1763.lean	feat: `congr` theorems using `Iff`	2022-10-26 18:00:24 -07:00
1763.lean.expected.out	fix: do not pretty print theorems with generalized field notation (#3750 )	2024-03-23 09:20:48 +00:00
1779.lean	feat: use `unop%` to implement unary minus notation	2022-10-26 06:55:24 -07:00
1779.lean.expected.out	feat: use `unop%` to implement unary minus notation	2022-10-26 06:55:24 -07:00
1781.lean	fix: bug in level normalization (soundness bug)	2022-10-26 05:22:26 -07:00
1781.lean.expected.out	fix: bug in level normalization (soundness bug)	2022-10-26 05:22:26 -07:00
1804.lean	feat: allow `doSeq` in `let x <- e \| seq`	2022-11-08 08:29:21 -08:00
1804.lean.expected.out	feat: allow `doSeq` in `let x <- e \| seq`	2022-11-08 08:29:21 -08:00
1825.lean	fix: integer overflows	2022-11-15 07:37:54 -08:00
1825.lean.expected.out	fix: integer overflows	2022-11-15 07:37:54 -08:00
1845.lean	fix: do method lifting across choice nodes	2022-11-21 17:52:14 +01:00
1845.lean.expected.out	fix: do method lifting across choice nodes	2022-11-21 17:52:14 +01:00
1856.lean	fix: fixes #1856	2022-11-18 19:34:32 -08:00
1856.lean.expected.out	chore: `pp.proofs.withType` is now false by default (#3379 )	2024-02-17 15:09:24 +00:00
1870.lean	fix: fixes #1870	2022-11-23 05:49:19 -08:00
1870.lean.expected.out	fix: fixes #2011	2023-01-05 17:33:45 -08:00
1878.lean	test: for #1878	2022-11-24 13:03:45 -08:00
1878.lean.expected.out	test: for #1878	2022-11-24 13:03:45 -08:00
1891.lean	fix: fixes #1891	2022-11-29 08:59:46 -08:00
1891.lean.expected.out	fix: fixes #1891	2022-11-29 08:59:46 -08:00
1918.lean	fix: remove repeat calls to `inferType` in `ignoreField`	2023-05-15 09:35:44 -07:00
1918.lean.expected.out	fix: remove repeat calls to `inferType` in `ignoreField`	2023-05-15 09:35:44 -07:00
1971.lean	feat: include unexpected token in error message	2023-09-12 11:42:24 +02:00
1971.lean.expected.out	feat: custom error recovery in parser (#3413 )	2024-02-21 14:29:54 +00:00
2005.lean	fix: be more careful with `MatchResult.uncovered` in syntax match	2023-01-09 13:05:00 +01:00
2005.lean.expected.out	fix: be more careful with `MatchResult.uncovered` in syntax match	2023-01-09 13:05:00 +01:00
2006.lean	fix: fixes #2006	2023-01-04 08:19:22 -08:00
2006.lean.expected.out	fix: fixes #2006	2023-01-04 08:19:22 -08:00
2040.lean	fix: make `^` a right action, add NatPow and HomogeneousPow	2023-11-12 16:57:51 +11:00
2040.lean.expected.out	fix: type class issues with `maxSynthPendingDepth := 1` (#4119 )	2024-05-14 03:03:32 +00:00
2045.lean	feat: apply app unexpanders for all prefixes of an application (#3375 )	2024-02-27 07:04:17 +00:00
2045.lean.expected.out	fix: notation unexpander on overapplication of non-nullary notation	2023-01-26 13:05:33 +01:00
2077.lean	fix: fixes #2077	2023-06-30 19:26:00 -07:00
2077.lean.expected.out	fix: fixes #2077	2023-06-30 19:26:00 -07:00
2115.lean	chore: fix test file names	2023-07-01 06:20:36 -07:00
2115.lean.expected.out	chore: fix test file names	2023-07-01 06:20:36 -07:00
2125.lean	fix: reject occurrences of inductive type in index	2023-02-28 12:22:54 -08:00
2125.lean.expected.out	fix: reject occurrences of inductive type in index	2023-02-28 12:22:54 -08:00
2161.lean	fix: `match` discriminant reduction should not unfold irreducible defs	2023-04-10 21:09:04 -07:00
2161.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
2178.lean	fix: fixes #2178 (#2784 )	2023-10-30 15:06:56 +11:00
2178.lean.expected.out	fix: fixes #2178 (#2784 )	2023-10-30 15:06:56 +11:00
2220.lean	fix: make `^` a right action, add NatPow and HomogeneousPow	2023-11-12 16:57:51 +11:00
2220.lean.expected.out	fix: type class issues with `maxSynthPendingDepth := 1` (#4119 )	2024-05-14 03:03:32 +00:00
2273.lean	feat: add flag for apply to defer failed typeclass syntheses as goals	2023-06-19 20:07:07 -07:00
2273.lean.expected.out	fix: type class issues with `maxSynthPendingDepth := 1` (#4119 )	2024-05-14 03:03:32 +00:00
2361.lean	feat: withAssignableSyntheticOpaque in assumption (#2596 )	2023-10-30 04:00:52 +00:00
2361.lean.expected.out	feat: withAssignableSyntheticOpaque in assumption (#2596 )	2023-10-30 04:00:52 +00:00
2505.lean	chore: fix MVarId.getType' (#2595 )	2023-10-09 11:04:33 +00:00
2505.lean.expected.out	chore: fix MVarId.getType' (#2595 )	2023-10-09 11:04:33 +00:00
2514.lean	fix: dsimp missing consumeMData when closing goals by rfl (#2776 )	2023-10-30 09:32:32 +11:00
2514.lean.expected.out	fix: dsimp missing consumeMData when closing goals by rfl (#2776 )	2023-10-30 09:32:32 +11:00
2634.lean	fix: `simp` fails when custom discharger makes no progress (#3317 )	2024-02-17 13:42:04 +00:00
2634.lean.expected.out	fix: `simp` fails when custom discharger makes no progress (#3317 )	2024-02-17 13:42:04 +00:00
3057.lean	fix: manage all declarations in a given derive (#3058 )	2024-01-09 07:42:06 +00:00
3057.lean.expected.out	fix: eta-expanded instances at `SynthInstance.lean` (#3638 )	2024-03-08 20:37:38 +00:00
3140.lean	fix: `derive BEq` on structure with `Prop`-fields (#3191 )	2024-01-18 02:32:51 +00:00
3140.lean.expected.out	fix: `derive BEq` on structure with `Prop`-fields (#3191 )	2024-01-18 02:32:51 +00:00
3989_1.lean	fix: `match_expr` parser (#4007 )	2024-04-27 23:56:28 +00:00
3989_1.lean.expected.out	fix: `match_expr` parser (#4007 )	2024-04-27 23:56:28 +00:00
3989_2.lean	fix: `match_expr` parser (#4007 )	2024-04-27 23:56:28 +00:00
3989_2.lean.expected.out	fix: `match_expr` parser (#4007 )	2024-04-27 23:56:28 +00:00
4089.lean	feat: relaxed reset/reuse in the code generator (#4100 )	2024-05-07 22:08:32 +00:00
4089.lean.expected.out	feat: relaxed reset/reuse in the code generator (#4100 )	2024-05-07 22:08:32 +00:00
4117.lean	fix: add `checkSystem` and `withIncRecDepth` to `withAutoBoundImplicit` (#4128 )	2024-05-10 21:55:26 +00:00
4117.lean.expected.out	fix: add `checkSystem` and `withIncRecDepth` to `withAutoBoundImplicit` (#4128 )	2024-05-10 21:55:26 +00:00
abst.lean
abst.lean.expected.out
allFieldForConstants.lean	chore: upstream Std.Data.List.Init.Lemmas (#3341 )	2024-02-15 03:19:23 +00:00
allFieldForConstants.lean.expected.out
ambiguousOpenExport.lean
ambiguousOpenExport.lean.expected.out
antiquotRecovery.lean
antiquotRecovery.lean.expected.out	feat: include unexpected token in error message	2023-09-12 11:42:24 +02:00
appParserIssue.lean
appParserIssue.lean.expected.out
argNameAtPlaceholderError.lean
argNameAtPlaceholderError.lean.expected.out	chore: fix tests after hash change	2022-12-01 20:18:14 -08:00
argNameIfMacroScopes.lean
argNameIfMacroScopes.lean.expected.out
arrayGetU.lean
arrayGetU.lean.expected.out	fix: do not pretty print theorems with generalized field notation (#3750 )	2024-03-23 09:20:48 +00:00
attrCmd.lean
attrCmd.lean.expected.out	fix: type class issues with `maxSynthPendingDepth := 1` (#4119 )	2024-05-14 03:03:32 +00:00
autobound_and_macroscopes.lean
autobound_and_macroscopes.lean.expected.out
autoBoundErrorMsg.lean
autoBoundErrorMsg.lean.expected.out
autoBoundImplicits1.lean	feat: allow upper case single character identifiers when relaxedAutoImplicit false (#2277 )	2023-06-19 20:04:09 -07:00
autoBoundImplicits1.lean.expected.out	feat: use signature pretty printer in `#check id`/`#check @id`	2022-12-21 21:59:05 +01:00
autoBoundImplicits2.lean
autoBoundImplicits2.lean.expected.out	feat: make `#check <ident>` always show the signature without elaboration	2022-12-21 21:59:05 +01:00
autoBoundPostponeLoop.lean
autoBoundPostponeLoop.lean.expected.out
autoImplicitChain.lean
autoImplicitChain.lean.expected.out
autoImplicitChainNameIssue.lean	feat: make `#check <ident>` always show the signature without elaboration	2022-12-21 21:59:05 +01:00
autoImplicitChainNameIssue.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
autoImplicitCtorParamIssue.lean
autoImplicitCtorParamIssue.lean.expected.out
autoImplicitForbidden.lean
autoImplicitForbidden.lean.expected.out
autoIssue.lean	feat: make `#check <ident>` always show the signature without elaboration	2022-12-21 21:59:05 +01:00
autoIssue.lean.expected.out	feat: apply app unexpanders for all prefixes of an application (#3375 )	2024-02-27 07:04:17 +00:00
autoPPExplicit.lean
autoPPExplicit.lean.expected.out
auxDeclIssue.lean
auxDeclIssue.lean.expected.out	chore: fix tests	2022-10-11 17:24:35 -07:00
badBinderName.lean
badBinderName.lean.expected.out
badIhName.lean
badIhName.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
beginEndAsMacro.lean
beginEndAsMacro.lean.expected.out
bigUnivOffsets.lean
bigUnivOffsets.lean.expected.out
binder_predicates.lean	chore: upstream Std.Util.ExtendedBinders (#3320 )	2024-02-14 11:36:00 +00:00
binder_predicates.lean.expected.out	chore: upstream Std.Util.ExtendedBinders (#3320 )	2024-02-14 11:36:00 +00:00
binderCacheIssue.lean
binderCacheIssue.lean.expected.out	feat: make `#check <ident>` always show the signature without elaboration	2022-12-21 21:59:05 +01:00
binderCacheIssue2.lean
binderCacheIssue2.lean.expected.out
bindersAbstractingUnassignedMVars.lean
bindersAbstractingUnassignedMVars.lean.expected.out
binop_at_pattern_issue.lean	chore: move `BitVec` to top level namespace	2024-02-23 15:15:57 -08:00
binop_at_pattern_issue.lean.expected.out	fix: match pattern missing test	2024-02-21 05:14:26 -08:00
binop_lazy.lean	fix: lazy_binop + coercion bug	2023-07-01 06:05:25 -07:00
binop_lazy.lean.expected.out
binopInfoTree.lean	fix: `binop%` info tree	2023-01-16 08:33:58 -08:00
binopInfoTree.lean.expected.out	fix: don't use info nodes before cursor for completion (#3778 )	2024-04-02 08:49:24 +00:00
binopIssues.lean	chore: upstream Std.Data.Int.Init modules (#3364 )	2024-02-16 03:58:23 +00:00
binopIssues.lean.expected.out	chore: upstream NatCast and IntCast (#3347 )	2024-02-16 00:54:22 +00:00
binopQuotPrecheck.lean	feat: add `quot_precheck` for expression tree elaborators (`binop%`, etc.) (#3078 )	2023-12-18 16:52:49 +00:00
binopQuotPrecheck.lean.expected.out	feat: add `quot_precheck` for expression tree elaborators (`binop%`, etc.) (#3078 )	2023-12-18 16:52:49 +00:00
binrel_binop.lean
binrel_binop.lean.expected.out	chore: upstream NatCast and IntCast (#3347 )	2024-02-16 00:54:22 +00:00
binrelTypeMismatch.lean	fix: expression tree elaborator for relations now localizes error messages to the LHS or RHS (#3442 )	2024-03-04 00:53:32 +00:00
binrelTypeMismatch.lean.expected.out	fix: expression tree elaborator for relations now localizes error messages to the LHS or RHS (#3442 )	2024-03-04 00:53:32 +00:00
binsearch.lean
binsearch.lean.expected.out
bintreeGoal.lean	chore: fix proofs and test	2024-02-09 09:57:57 +11:00
bintreeGoal.lean.expected.out	refactor: move `if-then-else` tactic to `Init`	2024-02-09 09:57:57 +11:00
bitwise.lean
bitwise.lean.expected.out
bool_simp.lean	chore: bool and prop lemmas for Mathlib compatibility and improved confluence (#3508 )	2024-03-04 23:56:30 +00:00
bool_simp.lean.expected.out	chore: bool and prop lemmas for Mathlib compatibility and improved confluence (#3508 )	2024-03-04 23:56:30 +00:00
builtinSimprocTrace.lean	fix: trace used builtin `simproc`s even if they are not in the environment	2024-01-09 12:57:15 +01:00
builtinSimprocTrace.lean.expected.out	fix: trace used builtin `simproc`s even if they are not in the environment	2024-01-09 12:57:15 +01:00
byCasesMetaM.lean	refactor: improve `MVarId` method discoverability	2022-07-27 17:49:00 -07:00
byCasesMetaM.lean.expected.out	chore: fix tests	2022-08-15 08:55:25 -07:00
byStrictIndent.lean	chore: tests for strict-indent nested by-s	2022-11-08 08:30:42 -08:00
byStrictIndent.lean.expected.out	feat: include unexpected token in error message	2023-09-12 11:42:24 +02:00
bytearray.lean	fix: toUInt64LE! and toUInt64BE! are swapped (#3660 )	2024-03-28 01:13:42 +00:00
bytearray.lean.expected.out	feat: ByteArray.hash	2022-12-01 20:18:14 -08:00
cacheIssue.lean
cacheIssue.lean.expected.out
calcErrors.lean	fix: enforce linebreak between `calc` steps	2023-09-18 05:39:41 -04:00
calcErrors.lean.expected.out	fix: type class issues with `maxSynthPendingDepth := 1` (#4119 )	2024-05-14 03:03:32 +00:00
casesOnCases.lean	chore: fix and disable some LCNF tests	2022-08-24 14:12:27 -07:00
casesOnCases.lean.expected.out	chore: fix and disable some LCNF tests	2022-08-24 14:12:27 -07:00
caseSuggestions.lean	feat: type of theorems must be propositions	2024-03-13 12:37:58 -07:00
caseSuggestions.lean.expected.out	feat: list the valid case tags when the user writes an invalid one	2023-10-06 11:14:21 +02:00
cdotAtSimpArg.lean	fix: look through binop% variants in `elabCDotFunctionAlias?`	2023-11-12 16:57:51 +11:00
cdotAtSimpArg.lean.expected.out	fix: look through binop% variants in `elabCDotFunctionAlias?`	2023-11-12 16:57:51 +11:00
cdotTuple.lean
cdotTuple.lean.expected.out
class_def_must_fail.lean
class_def_must_fail.lean.expected.out
classBadOutParam.lean
classBadOutParam.lean.expected.out
coe.lean	fix: extended `coe` notation and delaborator (#3295 )	2024-02-10 04:58:28 +00:00
coe.lean.expected.out	fix: extended `coe` notation and delaborator (#3295 )	2024-02-10 04:58:28 +00:00
coeAttr1.lean	chore: upstream Std.Tactic.CoeExt to Lean.Elab.CoeExt (#3280 )	2024-02-09 04:55:49 +00:00
coeAttr1.lean.expected.out	chore: upstream Std.Tactic.CoeExt to Lean.Elab.CoeExt (#3280 )	2024-02-09 04:55:49 +00:00
coeM.lean	fix: make `Lean.Internal.liftCoeM` and `Lean.Internal.coeM` unfold (#3404 )	2024-02-27 22:17:46 +00:00
coeM.lean.expected.out	fix: make `Lean.Internal.liftCoeM` and `Lean.Internal.coeM` unfold (#3404 )	2024-02-27 22:17:46 +00:00
collectDepsIssue.lean
collectDepsIssue.lean.expected.out
commandPrefix.lean
commandPrefix.lean.expected.out	feat: include unexpected token in error message	2023-09-12 11:42:24 +02:00
computedFieldsCode.lean	chore: snake-case attributes (part 1)	2022-10-19 09:28:08 -07:00
computedFieldsCode.lean.expected.out
congrThm.lean	feat: avoid `[Decidable p]` instance implicit parameters in congruence theorems when possible	2022-08-02 04:47:42 -07:00
congrThm.lean.expected.out	chore: `pp.proofs.withType` is now false by default (#3379 )	2024-02-17 15:09:24 +00:00
congrThmIssue.lean
congrThmIssue.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
constDelab.lean
constDelab.lean.expected.out
constructorTac.lean
constructorTac.lean.expected.out
consumePPHint.lean
consumePPHint.lean.expected.out
conv1.lean	feat: in conv tactic, use `try with_reducibe rfl` (#3763 )	2024-03-29 11:59:45 +00:00
conv1.lean.expected.out	feat: in conv tactic, use `try with_reducibe rfl` (#3763 )	2024-03-29 11:59:45 +00:00
convInConv.lean	feat: in conv tactic, use `try with_reducibe rfl` (#3763 )	2024-03-29 11:59:45 +00:00
convInConv.lean.expected.out	feat: in conv tactic, use `try with_reducibe rfl` (#3763 )	2024-03-29 11:59:45 +00:00
convPatternAtLetIssue.lean	feat: in conv tactic, use `try with_reducibe rfl` (#3763 )	2024-03-29 11:59:45 +00:00
convPatternAtLetIssue.lean.expected.out
convPatternMatchIssue.lean	feat: in conv tactic, use `try with_reducibe rfl` (#3763 )	2024-03-29 11:59:45 +00:00
convPatternMatchIssue.lean.expected.out
convZetaLetExt.lean
convZetaLetExt.lean.expected.out
copy-produced	chore: default `compiler.enableNew` to false until development restarts (#3034 )	2023-12-21 07:48:25 +00:00
csimpAttr.lean
csimpAttr.lean.expected.out
csimpAttrAppend.lean
csimpAttrAppend.lean.expected.out
ctor_layout.lean	chore: split up & simplify `importModules`	2023-08-31 15:37:33 -04:00
ctor_layout.lean.expected.out
ctorUnivTooBig.lean	feat: make `#check <ident>` always show the signature without elaboration	2022-12-21 21:59:05 +01:00
ctorUnivTooBig.lean.expected.out	feat: use signature pretty printer in `#check id`/`#check @id`	2022-12-21 21:59:05 +01:00
dbgMacros.lean
dbgMacros.lean.expected.out
decEqMutualInductives.lean	feat : derive `DecidableEq` for mutual inductives (#2591 )	2023-10-03 02:17:13 +00:00
decEqMutualInductives.lean.expected.out	fix: DecidableEq deriving handler could not handle fields whose types start with an implicit argument (#2918 )	2023-11-20 20:51:47 +11:00
decideTactic.lean	feat: improve error messages and docstring for `decide` tactic (#3422 )	2024-02-27 23:07:38 +00:00
decideTactic.lean.expected.out	feat: improve error messages and docstring for `decide` tactic (#3422 )	2024-02-27 23:07:38 +00:00
decimals.lean
decimals.lean.expected.out
decreasing_by.lean	feat: improve termination_by error messages (#3255 )	2024-02-05 13:13:53 +00:00
decreasing_by.lean.expected.out	fix: make tests be aware of new instance names (#3936 )	2024-04-17 16:14:51 +02:00
defaultInstance.lean	chore: snake-case attributes (part 1)	2022-10-19 09:28:08 -07:00
defaultInstance.lean.expected.out	fix: type class issues with `maxSynthPendingDepth := 1` (#4119 )	2024-05-14 03:03:32 +00:00
defaultInstanceWithPrio.lean	chore: snake-case attributes (part 1)	2022-10-19 09:28:08 -07:00
defaultInstanceWithPrio.lean.expected.out
defInst.lean
defInst.lean.expected.out	fix: type class issues with `maxSynthPendingDepth := 1` (#4119 )	2024-05-14 03:03:32 +00:00
delabApp.lean	feat: apply app unexpanders for all prefixes of an application (#3375 )	2024-02-27 07:04:17 +00:00
delabApp.lean.expected.out	feat: apply app unexpanders for all prefixes of an application (#3375 )	2024-02-27 07:04:17 +00:00
delabDoLetFun.lean	feat: delaborate `have` inside `do` blocks (#3116 )	2024-01-02 09:36:39 +00:00
delabDoLetFun.lean.expected.out	feat: delaborate `have` inside `do` blocks (#3116 )	2024-01-02 09:36:39 +00:00
delabOverApp.lean	feat: apply app unexpanders for all prefixes of an application (#3375 )	2024-02-27 07:04:17 +00:00
delabOverApp.lean.expected.out	feat: apply app unexpanders for all prefixes of an application (#3375 )	2024-02-27 07:04:17 +00:00
delabUnexpand.lean	chore: snake-case attributes (part 1)	2022-10-19 09:28:08 -07:00
delabUnexpand.lean.expected.out
delta.lean
delta.lean.expected.out	feat: multiple `delta` (part 2)	2022-09-21 18:04:31 -07:00
deltaRedIndPredBelow.lean	fix: missing `whnf` in `mkBelowBinder` and `mkMotiveBinder` (#2991 )	2023-12-01 14:46:09 +00:00
deltaRedIndPredBelow.lean.expected.out	fix: missing `whnf` in `mkBelowBinder` and `mkMotiveBinder` (#2991 )	2023-12-01 14:46:09 +00:00
deprecated.lean	fix: generate deprecation warnings for dot notation (#3969 )	2024-05-09 04:52:09 +00:00
deprecated.lean.expected.out	feat: improve @[deprecated] attr (#3968 )	2024-04-23 17:00:32 +00:00
derivingDecidableEq.lean
derivingDecidableEq.lean.expected.out
derivingHashable.lean	fix: add local Hashable instance (fixes #1737 )	2022-10-23 21:26:04 +02:00
derivingHashable.lean.expected.out	chore: fix tests after hash change	2022-12-01 20:18:14 -08:00
derivingRpcEncoding.lean	feat: bundle of widget improvements (#2964 )	2023-12-21 06:24:33 +00:00
derivingRpcEncoding.lean.expected.out	feat: bundle of widget improvements (#2964 )	2023-12-21 06:24:33 +00:00
diamond1.lean
diamond1.lean.expected.out	feat: `#print` command shows structure fields (#3768 )	2024-04-24 03:18:09 +00:00
diamond2.lean	feat: make `#check <ident>` always show the signature without elaboration	2022-12-21 21:59:05 +01:00
diamond2.lean.expected.out	feat: flatten parent projections when pretty printing structure instance notation (#3749 )	2024-03-23 09:20:52 +00:00
diamond3.lean
diamond3.lean.expected.out	feat: delaboration collapses parent projections (#3326 )	2024-02-14 23:44:48 +00:00
diamond4.lean
diamond4.lean.expected.out	fix: fixes #1907	2022-12-02 08:59:16 -08:00
diamond5.lean	feat: make `#check <ident>` always show the signature without elaboration	2022-12-21 21:59:05 +01:00
diamond5.lean.expected.out	feat: use signature pretty printer in `#check id`/`#check @id`	2022-12-21 21:59:05 +01:00
diamond6.lean	feat: make `#check <ident>` always show the signature without elaboration	2022-12-21 21:59:05 +01:00
diamond6.lean.expected.out	feat: use signature pretty printer in `#check id`/`#check @id`	2022-12-21 21:59:05 +01:00
diamond7.lean	feat: make `#check <ident>` always show the signature without elaboration	2022-12-21 21:59:05 +01:00
diamond7.lean.expected.out	feat: use signature pretty printer in `#check id`/`#check @id`	2022-12-21 21:59:05 +01:00
diamond8.lean
diamond8.lean.expected.out	feat: `#print` command shows structure fields (#3768 )	2024-04-24 03:18:09 +00:00
diamond9.lean
diamond9.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
diamond10.lean
diamond10.lean.expected.out
discrTreeIota.lean	feat: do not perform iota reduction at the discrimination tree module	2022-11-15 16:47:12 -08:00
discrTreeIota.lean.expected.out	feat: do not perform iota reduction at the discrimination tree module	2022-11-15 16:47:12 -08:00
docStr.lean	fix: `add_decl_doc` should check that declarations are local (#3311 )	2024-02-12 12:04:51 +00:00
docStr.lean.expected.out	feat: add `cleanupAnnotations` parameter to `forallTelescope` methods (#4180 )	2024-05-15 22:19:07 +00:00
doErrorMsg.lean
doErrorMsg.lean.expected.out	chore: remove dangerous instances	2022-12-21 04:24:39 +01:00
doIfLet.lean	feat: support `let mut x := e \| alt`	2022-08-10 06:29:49 -07:00
doIfLet.lean.expected.out	feat: support `let mut x := e \| alt`	2022-08-10 06:29:49 -07:00
doIssue.lean
doIssue.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
doLetLoop.lean
doLetLoop.lean.expected.out
doNotation1.lean
doNotation1.lean.expected.out	fix: improve "`{varName}` cannot be reassigned" error message	2022-07-24 07:44:34 -07:00
doSeqRightIssue.lean
doSeqRightIssue.lean.expected.out
doubleReset.lean	fix: double `reset` bug at `ResetReuse` (#4028 )	2024-04-29 23:26:07 +00:00
doubleReset.lean.expected.out	fix: double `reset` bug at `ResetReuse` (#4028 )	2024-04-29 23:26:07 +00:00
dsimpViaConst.lean	test: ensure `dsimp` can use `rfl` thm constants	2023-10-20 19:06:40 -07:00
dsimpViaConst.lean.expected.out	test: ensure `dsimp` can use `rfl` thm constants	2023-10-20 19:06:40 -07:00
dsimpZetaIssue.lean	feat: enable failIfUnchanged by default in simp	2023-08-16 10:14:23 -07:00
dsimpZetaIssue.lean.expected.out
eagerCoeExpansion.lean
eagerCoeExpansion.lean.expected.out	feat: extract `delabAppCore`, define `withOverApp`, and make over-applied projections pretty print (#3083 )	2024-01-10 13:24:28 +00:00
eagerUnfoldingIssue.lean
eagerUnfoldingIssue.lean.expected.out	fix: type class issues with `maxSynthPendingDepth := 1` (#4119 )	2024-05-14 03:03:32 +00:00
elabAsElim.lean	fix: fixes #1851	2022-11-19 07:01:02 -08:00
elabAsElim.lean.expected.out	feat: add `[elabAsElim]` elaboration strategy	2022-07-28 20:08:29 -07:00
ellipsisProjIssue.lean	fix: disallow `.` immediately after `..`	2022-10-26 07:13:40 -07:00
ellipsisProjIssue.lean.expected.out	fix: disallow `.` immediately after `..`	2022-10-26 07:13:40 -07:00
elseifDoErrorPos.lean
elseifDoErrorPos.lean.expected.out	fix: preserve condition position info in `if`	2022-08-13 18:07:30 -07:00
emptyc.lean
emptyc.lean.expected.out
emptyTypeAscription.lean	feat: empty type ascription syntax `(e :)` (part 2)	2022-11-07 19:10:56 +01:00
emptyTypeAscription.lean.expected.out	feat: empty type ascription syntax `(e :)` (part 2)	2022-11-07 19:10:56 +01:00
eoi.lean
eoi.lean.expected.out
eraseInsts.lean
eraseInsts.lean.expected.out	fix: type class issues with `maxSynthPendingDepth := 1` (#4119 )	2024-05-14 03:03:32 +00:00
eraseSimp.lean	feat: enable failIfUnchanged by default in simp	2023-08-16 10:14:23 -07:00
eraseSimp.lean.expected.out
errorOnInductionForNested.lean
errorOnInductionForNested.lean.expected.out
errorRecoveryBug.lean
errorRecoveryBug.lean.expected.out
eta.lean
eta.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
etaStructIssue.lean
etaStructIssue.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
eval_except.lean
eval_except.lean.expected.out
evalCmd.lean
evalCmd.lean.expected.out
evalInstMessage.lean
evalInstMessage.lean.expected.out
evalLeak.lean	fix: `#eval` command was leaking auxiliary declarations into the environment (#3323 )	2024-02-13 21:44:52 +00:00
evalLeak.lean.expected.out	fix: `#eval` command was leaking auxiliary declarations into the environment (#3323 )	2024-02-13 21:44:52 +00:00
evalNone.lean
evalNone.lean.expected.out	chore: fix tests after hash change	2022-12-01 20:18:14 -08:00
evalSorry.lean
evalSorry.lean.expected.out
evalWithMVar.lean
evalWithMVar.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
exactErrorPos.lean
exactErrorPos.lean.expected.out
exceptionalTrace.lean	fix: broken trace tree on elab runtime exception (#3371 )	2024-02-19 11:15:23 +00:00
exceptionalTrace.lean.expected.out	chore: fix tests	2024-05-01 03:19:39 +02:00
exitAfterParseError.lean
exitAfterParseError.lean.expected.out	feat: include unexpected token in error message	2023-09-12 11:42:24 +02:00
expandExplicitBinders.lean	fix: unhygiene in `expandExplicitBinders`	2023-02-22 17:07:31 +01:00
expandExplicitBinders.lean.expected.out	fix: unhygiene in `expandExplicitBinders`	2023-02-22 17:07:31 +01:00
extract.lean
extract.lean.expected.out
failTac.lean
failTac.lean.expected.out
file_not_found.lean
file_not_found.lean.expected.out
filePath.lean	fix: update System.FilePath.parent to handle edge cases for absolute paths (#3645 )	2024-03-26 05:09:44 +00:00
filePath.lean.expected.out	fix: update System.FilePath.parent to handle edge cases for absolute paths (#3645 )	2024-03-26 05:09:44 +00:00
fixedIndexToParamIssue.lean
fixedIndexToParamIssue.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
fixedIndicesToParams.lean
fixedIndicesToParams.lean.expected.out
forallMetaBounded.lean
forallMetaBounded.lean.expected.out	test: strip some more indices	2022-07-25 08:01:27 -07:00
forErrors.lean
forErrors.lean.expected.out	fix: type class issues with `maxSynthPendingDepth := 1` (#4119 )	2024-05-14 03:03:32 +00:00
Format.lean
Format.lean.expected.out
formatTerm.lean	fix: trailing whitespace in `location` formatter (#3318 )	2024-02-13 15:53:29 +00:00
formatTerm.lean.expected.out	fix: trailing whitespace in `location` formatter (#3318 )	2024-02-13 15:53:29 +00:00
fun.lean
fun.lean.expected.out
funExpected.lean
funExpected.lean.expected.out
funind_errors.lean	feat: use reserved name infrastructure for functional induction (#3776 )	2024-03-26 22:25:10 +00:00
funind_errors.lean.expected.out	feat: use reserved name infrastructure for functional induction (#3776 )	2024-03-26 22:25:10 +00:00
funind_reserved.lean	fix: check that funind-reserved names are available (#4135 )	2024-05-12 20:39:14 +00:00
funind_reserved.lean.expected.out	fix: check that funind-reserved names are available (#4135 )	2024-05-12 20:39:14 +00:00
funInfoBug.lean	chore: move Std.* data structures to Lean.*	2022-09-26 05:46:04 -07:00
funInfoBug.lean.expected.out	chore: move Std.* data structures to Lean.*	2022-09-26 05:46:04 -07:00
funParen.lean
funParen.lean.expected.out	chore: snake-case attributes (part 1)	2022-10-19 09:28:08 -07:00
gcd.lean
gcd.lean.expected.out
getElem.lean	feat: use omega in the get_elem tactic (#3515 )	2024-02-27 18:52:04 +00:00
getElem.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
guessLex.lean	refactor: pass Measures around as Expr in GuessLex (#3665 )	2024-03-16 10:25:55 +00:00
guessLex.lean.expected.out	refactor: pass Measures around as Expr in GuessLex (#3665 )	2024-03-16 10:25:55 +00:00
guessLexDiff.lean	feat: infer termination arguments like `xs.size - i` (#3666 )	2024-03-16 12:27:35 +00:00
guessLexDiff.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
guessLexFailures.lean	feat: per-function termination hints	2024-01-10 17:27:35 +01:00
guessLexFailures.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
guessLexTricky.lean	feat: per-function termination hints	2024-01-10 17:27:35 +01:00
guessLexTricky.lean.expected.out	feat: GuessLex: avoid writing `sizeOf` in termination argument when not needed (#3630 )	2024-03-10 22:57:10 +00:00
guessLexTricky2.lean	feat: GuessLex: print inferred termination argument (#3012 )	2023-12-05 09:41:52 +00:00
guessLexTricky2.lean.expected.out	refactor: termination arguments as Expr, not Syntax (#3658 )	2024-03-14 23:51:53 +00:00
have.lean
have.lean.expected.out	feat: include unexpected token in error message	2023-09-12 11:42:24 +02:00
hidingInaccessibleNames.lean
hidingInaccessibleNames.lean.expected.out	chore: default `compiler.enableNew` to false until development restarts (#3034 )	2023-12-21 07:48:25 +00:00
holeErrors.lean
holeErrors.lean.expected.out	chore: fix tests after hash change	2022-12-01 20:18:14 -08:00
holes.lean
holes.lean.expected.out	chore: default `compiler.enableNew` to false until development restarts (#3034 )	2023-12-21 07:48:25 +00:00
hpow.lean	chore: typos (#4026 )	2024-04-29 14:04:50 +00:00
hpow.lean.expected.out	chore: upstream NatCast and IntCast (#3347 )	2024-02-16 00:54:22 +00:00
hygienicIntro.lean
hygienicIntro.lean.expected.out
implementedByIssue.lean	chore: snake-case attributes (part 1)	2022-10-19 09:28:08 -07:00
implementedByIssue.lean.expected.out	chore: snake-case attributes (part 1)	2022-10-19 09:28:08 -07:00
implicitLambdaIssue.lean
implicitLambdaIssue.lean.expected.out
implicitTypePos.lean
implicitTypePos.lean.expected.out	chore: fix tests	2022-11-30 17:52:37 -08:00
indimpltarget.lean	feat: induction using <term> (#3188 )	2024-01-25 16:57:41 +00:00
indimpltarget.lean.expected.out	feat: induction using <term> (#3188 )	2024-01-25 16:57:41 +00:00
inductionErrors.lean
inductionErrors.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
inductionGen.lean	fix: `checkTargets` check for duplicate target (#3171 )	2024-01-18 09:44:17 +00:00
inductionGen.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
inductionMutual.lean
inductionMutual.lean.expected.out
inductive1.lean
inductive1.lean.expected.out	feat: function coercions with unification	2022-10-14 12:08:10 -07:00
inductiveUnivErrorMsg.lean
inductiveUnivErrorMsg.lean.expected.out
indUsingTerm.lean	feat: induction using <term> (#3188 )	2024-01-25 16:57:41 +00:00
indUsingTerm.lean.expected.out	feat: induction using <term> (#3188 )	2024-01-25 16:57:41 +00:00
infoFromFailure.lean
infoFromFailure.lean.expected.out	chore: fix tests	2022-08-15 08:55:25 -07:00
inlineIssue.lean	chore: fix and disable some LCNF tests	2022-08-24 14:12:27 -07:00
inlineIssue.lean.expected.out	chore: fix and disable some LCNF tests	2022-08-24 14:12:27 -07:00
inst.lean
inst.lean.expected.out
instance1.lean	chore: add test	2022-09-13 06:19:40 -07:00
instance1.lean.expected.out	chore: add test	2022-09-13 06:19:40 -07:00
int_div_mod.lean	feat: introduce native functions for Int.ediv / Int.emod (#3376 )	2024-02-19 15:04:51 +00:00
int_div_mod.lean.expected.out	feat: introduce native functions for Int.ediv / Int.emod (#3376 )	2024-02-19 15:04:51 +00:00
intModBug.lean
intModBug.lean.expected.out
intNegSucc.lean
intNegSucc.lean.expected.out
introLetBug.lean
introLetBug.lean.expected.out
invalidEnd.lean	feat: report section name in invalid end msg	2023-06-09 14:41:39 -07:00
invalidEnd.lean.expected.out	feat: report section name in invalid end msg	2023-06-09 14:41:39 -07:00
invalidFieldName.lean
invalidFieldName.lean.expected.out
invalidInstImplicit.lean
invalidInstImplicit.lean.expected.out
invalidMutualError.lean	feat: detail error message about invalid mutual blocks (#2949 )	2023-12-05 10:50:10 +00:00
invalidMutualError.lean.expected.out	feat: detail error message about invalid mutual blocks (#2949 )	2023-12-05 10:50:10 +00:00
invalidNamedArgs.lean
invalidNamedArgs.lean.expected.out
invalidPatternIssue.lean
invalidPatternIssue.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
IRbug.lean
IRbug.lean.expected.out
isDefEqOffsetBug.lean
isDefEqOffsetBug.lean.expected.out
isNoncomputable.lean
isNoncomputable.lean.expected.out
issue2260.lean	fix: improve error message when termination argument is too dependent (#3414 )	2024-02-22 16:39:26 +00:00
issue2260.lean.expected.out	refactor: termination arguments as Expr, not Syntax (#3658 )	2024-03-14 23:51:53 +00:00
issue2981.lean	test: expand tests/lean/issue2981.lean a bit (#3007 )	2023-12-01 17:52:34 +00:00
issue2981.lean.expected.out	fix: make tests be aware of new instance names (#3936 )	2024-04-17 16:14:51 +02:00
jason2.lean
jason2.lean.expected.out	chore: flaky tests	2023-04-10 13:00:04 -07:00
json.lean	feat: fromJson? derivations now say where a parsing error occurred (#1656 )	2022-09-28 09:15:26 +00:00
json.lean.expected.out	feat: fromJson? derivations now say where a parsing error occurred (#1656 )	2022-09-28 09:15:26 +00:00
kernelMVarBug.lean
kernelMVarBug.lean.expected.out	fix: type class issues with `maxSynthPendingDepth := 1` (#4119 )	2024-05-14 03:03:32 +00:00
keyAttrErase.lean	chore: snake-case attributes (part 1)	2022-10-19 09:28:08 -07:00
keyAttrErase.lean.expected.out	chore: upstream norm_cast tactic (#3322 )	2024-02-19 17:49:17 -08:00
lazySeq.lean
lazySeq.lean.expected.out
lcnfTypes.lean	chore: fix tests	2022-10-13 06:16:56 -07:00
lcnfTypes.lean.expected.out	chore: extend GetElem with getElem! and getElem? (#3694 )	2024-03-28 01:42:00 +00:00
LE.lean	feat: make `#check <ident>` always show the signature without elaboration	2022-12-21 21:59:05 +01:00
LE.lean.expected.out	feat: use signature pretty printer in `#check id`/`#check @id`	2022-12-21 21:59:05 +01:00
lean3RefineBug.lean
lean3RefineBug.lean.expected.out	chore: fix tests	2022-10-11 17:24:35 -07:00
letArrowOutsideDo.lean
letArrowOutsideDo.lean.expected.out	feat: include unexpected token in error message	2023-09-12 11:42:24 +02:00
letFun.lean	feat: encode `let_fun` using a `letFun` function (#2973 )	2023-12-18 09:01:42 +00:00
letFun.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
letPatIssue.lean
letPatIssue.lean.expected.out
letrec1.lean
letrec1.lean.expected.out
letrecErrors.lean
letrecErrors.lean.expected.out
letRecTheorem.lean	feat: infer def/theorem DefKind for `let rec`	2022-11-29 08:16:47 -08:00
letRecTheorem.lean.expected.out	feat: infer def/theorem DefKind for `let rec`	2022-11-29 08:16:47 -08:00
librarySearch.lean	chore: Std -> Batteries renaming (#4108 )	2024-05-08 05:04:25 +00:00
librarySearch.lean.expected.out	chore: port librarySearch tests from std (#3530 )	2024-02-28 17:24:17 +00:00
liftOverLeft.lean
liftOverLeft.lean.expected.out
linterMissingDocs.lean	chore: snake-case attributes (part 1)	2022-10-19 09:28:08 -07:00
linterMissingDocs.lean.expected.out	feat: make linter options more explicitly discoverable (#3938 )	2024-04-18 07:20:55 +00:00
linterSuspiciousUnexpanderPatterns.lean	chore: snake-case attributes (part 1)	2022-10-19 09:28:08 -07:00
linterSuspiciousUnexpanderPatterns.lean.expected.out	feat: make linter options more explicitly discoverable (#3938 )	2024-04-18 07:20:55 +00:00
linterUnusedVariables.lean	perf: rewrite UnusedVariables lint (#3186 )	2024-03-21 12:28:57 +00:00
linterUnusedVariables.lean.expected.out	feat: make linter options more explicitly discoverable (#3938 )	2024-04-18 07:20:55 +00:00
listLength.lean
listLength.lean.expected.out
lit_values.lean	feat: add helper functions for recognizing builtin literals	2024-02-24 16:08:07 -08:00
lit_values.lean.expected.out	feat: add helper functions for recognizing builtin literals	2024-02-24 16:08:07 -08:00
ll_infer_type_bug.lean
ll_infer_type_bug.lean.expected.out	feat: `import` command stub	2022-10-12 11:11:31 -07:00
localNotationPP.lean
localNotationPP.lean.expected.out
longestParsePrio.lean	fix: prefer longer parse even if unsuccessful	2022-09-28 15:57:01 -07:00
longestParsePrio.lean.expected.out	fix: prefer longer parse even if unsuccessful	2022-09-28 15:57:01 -07:00
loopErrorRecovery.lean
loopErrorRecovery.lean.expected.out
lvl1.lean
lvl1.lean.expected.out
macroElabRulesIssue1.lean
macroElabRulesIssue1.lean.expected.out
macroElabRulesIssue2.lean
macroElabRulesIssue2.lean.expected.out	fix: ensure messages associated with last exception are not lost at `evalTactic`	2022-07-22 12:05:29 -04:00
macroError.lean
macroError.lean.expected.out
macroPrio.lean
macroPrio.lean.expected.out
macroResolveName.lean
macroResolveName.lean.expected.out	chore: unexpanders for `Name.mkStr` and `Array.mkArray`	2022-10-04 17:18:36 -07:00
macroscopes.lean
macroscopes.lean.expected.out
macroStack.lean
macroStack.lean.expected.out	fix: type class issues with `maxSynthPendingDepth := 1` (#4119 )	2024-05-14 03:03:32 +00:00
macroSwizzle.lean	fix: annotate all syntax nodes produced by quotations as synthetic	2022-08-13 18:07:30 -07:00
macroSwizzle.lean.expected.out	fix: type class issues with `maxSynthPendingDepth := 1` (#4119 )	2024-05-14 03:03:32 +00:00
macroTrace.lean
macroTrace.lean.expected.out
magical.lean
magical.lean.expected.out
mangling.lean
mangling.lean.expected.out
match1.lean
match1.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
match2.lean
match2.lean.expected.out
match3.lean
match3.lean.expected.out
match4.lean	fix: panic in Match.SimpH.substRHS	2023-05-28 17:04:28 -07:00
match4.lean.expected.out
matchAltIndent.lean
matchAltIndent.lean.expected.out
matchApp.lean
matchApp.lean.expected.out
matchErrorLocation.lean
matchErrorLocation.lean.expected.out
matchErrorMsg.lean
matchErrorMsg.lean.expected.out
matchLeftovers.lean
matchLeftovers.lean.expected.out	chore: fix tests	2022-10-11 17:24:35 -07:00
matchMissingCasesAsStuckError.lean
matchMissingCasesAsStuckError.lean.expected.out
matchMultAlt.lean	chore: add @[simp] to Nat.succ_eq_add_one, and cleanup downstream (#3579 )	2024-03-13 05:35:52 +00:00
matchMultAlt.lean.expected.out
matchOfNatIssue.lean	chore: change simp default to decide := false (#2722 )	2023-11-02 10:06:38 +11:00
matchOfNatIssue.lean.expected.out	chore: upstream Std.Data.Int.Init modules (#3364 )	2024-02-16 03:58:23 +00:00
matchOrIssue.lean
matchOrIssue.lean.expected.out	chore: snake-case attributes (part 1)	2022-10-19 09:28:08 -07:00
matchPatternInsideBinders.lean
matchPatternInsideBinders.lean.expected.out
matchPatternPartialApp.lean	feat: in conv tactic, use `try with_reducibe rfl` (#3763 )	2024-03-29 11:59:45 +00:00
matchPatternPartialApp.lean.expected.out
matchunit.lean
matchunit.lean.expected.out
matchUnknownFVarBug.lean
matchUnknownFVarBug.lean.expected.out
matchVarNames.lean
matchVarNames.lean.expected.out	chore: fix tests	2022-10-11 17:24:35 -07:00
metaEvalInstMessage.lean
metaEvalInstMessage.lean.expected.out
missingExplicitWithForwardNamedDep.lean
missingExplicitWithForwardNamedDep.lean.expected.out	feat: use signature pretty printer in `#check id`/`#check @id`	2022-12-21 21:59:05 +01:00
mkProjStx.lean
mkProjStx.lean.expected.out
modBug.lean
modBug.lean.expected.out
moduleDoc.lean
moduleDoc.lean.expected.out
moduleOf.lean	chore: move Std.* data structures to Lean.*	2022-09-26 05:46:04 -07:00
moduleOf.lean.expected.out	chore: move Bootstrap.Data -> Lean.Data	2022-08-31 11:48:57 -07:00
motiveNotTypeCorect.lean	refactor: rewrite: produce simpler proof terms (#3121 )	2024-01-19 07:20:58 +00:00
motiveNotTypeCorect.lean.expected.out	refactor: rewrite: produce simpler proof terms (#3121 )	2024-01-19 07:20:58 +00:00
mulcommErrorMessage.lean
mulcommErrorMessage.lean.expected.out	fix: make `elabTermEnsuringType` respect `errToSorry` when there is a type mismatch (#3633 )	2024-03-09 15:30:47 +00:00
multiConstantError.lean
multiConstantError.lean.expected.out	chore: fix tests	2022-11-30 17:52:37 -08:00
mutualdef1.lean
mutualdef1.lean.expected.out
mutualWithNamespaceMacro.lean	feat: multiple namespaces in mutual declarations	2022-08-04 19:18:49 -07:00
mutualWithNamespaceMacro.lean.expected.out	feat: multiple namespaces in mutual declarations	2022-08-04 19:18:49 -07:00
mutwf1.lean	feat: per-function termination hints	2024-01-10 17:27:35 +01:00
mutwf1.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
mutwftypemismatch.lean	refactor: ArgsPacker (#3621 )	2024-03-14 14:59:40 +00:00
mutwftypemismatch.lean.expected.out	refactor: termination arguments as Expr, not Syntax (#3658 )	2024-03-14 23:51:53 +00:00
mvar_fvar.lean
mvar_fvar.lean.expected.out
mvarAtDefaultValue.lean
mvarAtDefaultValue.lean.expected.out
nameArgErrorIssue.lean
nameArgErrorIssue.lean.expected.out
namedHoles.lean
namedHoles.lean.expected.out
namelit.lean
namelit.lean.expected.out	fix: mark `Lean.Name.mkStr*` functions as `[reducible]`	2022-09-29 17:36:30 -07:00
nameRepr.lean
nameRepr.lean.expected.out
negFloat.lean
negFloat.lean.expected.out
newCatPanic.lean
newCatPanic.lean.expected.out
nonAtomicFieldName.lean
nonAtomicFieldName.lean.expected.out
noncompSection.lean
noncompSection.lean.expected.out
nondepArrow.lean
nondepArrow.lean.expected.out
nonfatalattrs.lean
nonfatalattrs.lean.expected.out
nonReserved.lean
nonReserved.lean.expected.out	feat: include unexpected token in error message	2023-09-12 11:42:24 +02:00
noTabs.lean
noTabs.lean.expected.out	fix: extraneous `missing` items on parser stack	2022-11-11 09:13:02 +01:00
notationDelab.lean
notationDelab.lean.expected.out
notationPrecheck.lean
notationPrecheck.lean.expected.out	chore: snake-case attributes (part 1)	2022-10-19 09:28:08 -07:00
omega-failure.lean	feat: omega: more helpful error messages (#3847 )	2024-04-16 15:11:51 +00:00
omega-failure.lean.expected.out	feat: omega: more helpful error messages (#3847 )	2024-04-16 15:11:51 +00:00
openExport.lean
openExport.lean.expected.out	feat: use signature pretty printer in `#check id`/`#check @id`	2022-12-21 21:59:05 +01:00
openScoped.lean	feat: make `#check <ident>` always show the signature without elaboration	2022-12-21 21:59:05 +01:00
openScoped.lean.expected.out	fix: type class issues with `maxSynthPendingDepth := 1` (#4119 )	2024-05-14 03:03:32 +00:00
optionGetD.lean	fix: Option.getD eagerly evaluates dflt (#3043 )	2023-12-11 10:07:30 +00:00
optionGetD.lean.expected.out	fix: Option.getD eagerly evaluates dflt (#3043 )	2023-12-11 10:07:30 +00:00
or_shortcircuit.lean
or_shortcircuit.lean.expected.out
parserPrio.lean
parserPrio.lean.expected.out
parserRecovery.lean	feat: custom error recovery in parser (#3413 )	2024-02-21 14:29:54 +00:00
parserRecovery.lean.expected.out	feat: custom error recovery in parser (#3413 )	2024-02-21 14:29:54 +00:00
partialIssue.lean	feat: propagate `maxHeartbeats` to kernel (#4113 )	2024-05-09 17:44:19 +00:00
partialIssue.lean.expected.out	fix: kernel must ensure that `safe` functions cannot use `partial` ones.	2023-01-27 12:17:37 -08:00
partialSyntaxTraces.lean	feat: snapshot trees and language processors (#3014 )	2024-03-14 13:40:08 +00:00
partialSyntaxTraces.lean.expected.out	feat: snapshot trees and language processors (#3014 )	2024-03-14 13:40:08 +00:00
partialVariable.lean
partialVariable.lean.expected.out	feat: include unexpected token in error message	2023-09-12 11:42:24 +02:00
patvar.lean
patvar.lean.expected.out
phashmap_inst_coherence.lean	chore: move Std.* data structures to Lean.*	2022-09-26 05:46:04 -07:00
phashmap_inst_coherence.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
ppBeta.lean	feat: `pp.beta` to apply beta reduction when pretty printing (#2864 )	2023-11-24 12:26:31 +00:00
ppBeta.lean.expected.out	feat: `pp.beta` to apply beta reduction when pretty printing (#2864 )	2023-11-24 12:26:31 +00:00
ppDeepTerms.lean	fix: make omission syntax be a builtin syntax (part 2)	2024-02-28 09:23:17 +01:00
ppDeepTerms.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
ppExpr.lean
ppExpr.lean.expected.out
PPInstances.lean
PPInstances.lean.expected.out
ppite.lean
ppite.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
pplevel.lean
pplevel.lean.expected.out
ppMotives.lean
ppMotives.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
ppNotationCode.lean
ppNotationCode.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
ppNumericTypes.lean	feat: `pp.numericTypes` option for printing number literals with type ascriptions (#2933 )	2024-02-01 17:23:32 +11:00
ppNumericTypes.lean.expected.out	feat: `pp.numericTypes` option for printing number literals with type ascriptions (#2933 )	2024-02-01 17:23:32 +11:00
ppProofs.lean	feat: have `pp.proofs` use `⋯` for omission (#3241 )	2024-02-15 21:49:41 +00:00
ppProofs.lean.expected.out	chore: `pp.proofs.withType` is now false by default (#3379 )	2024-02-17 15:09:24 +00:00
PPRoundtrip.lean	chore: move Std.* data structures to Lean.*	2022-09-26 05:46:04 -07:00
PPRoundtrip.lean.expected.out	fix: fixes #1571	2022-09-15 11:16:16 -07:00
ppSyntax.lean
ppSyntax.lean.expected.out
ppUnicode.lean	feat: add `fun x ↦ y` syntax	2023-01-03 13:59:53 -08:00
ppUnicode.lean.expected.out	feat: add `fun x ↦ y` syntax	2023-01-03 13:59:53 -08:00
precissues.lean
precissues.lean.expected.out	feat: include unexpected token in error message	2023-09-12 11:42:24 +02:00
printStructure.lean	feat: `#print` command shows structure fields (#3768 )	2024-04-24 03:18:09 +00:00
printStructure.lean.expected.out	feat: `#print` command shows structure fields (#3768 )	2024-04-24 03:18:09 +00:00
private.lean
private.lean.expected.out	fix: `private` + `pp.fullNames`	2022-12-21 21:59:05 +01:00
privateFieldCopyIssue.lean
privateFieldCopyIssue.lean.expected.out
Process.lean
Process.lean.expected.out	feat: `import` command stub	2022-10-12 11:11:31 -07:00
promise.lean	chore: add test	2022-09-05 08:52:46 -07:00
promise.lean.expected.out	chore: add test	2022-09-05 08:52:46 -07:00
protected.lean
protected.lean.expected.out	feat: use signature pretty printer in `#check id`/`#check @id`	2022-12-21 21:59:05 +01:00
protectedAlias.lean
protectedAlias.lean.expected.out	feat: use signature pretty printer in `#check id`/`#check @id`	2022-12-21 21:59:05 +01:00
prvCtor.lean	feat: make `Environment.mk` private (#2604 )	2023-10-04 22:02:54 +11:00
prvCtor.lean.expected.out	fix: type class issues with `maxSynthPendingDepth := 1` (#4119 )	2024-05-14 03:03:32 +00:00
prvNameWithMacroScopes.lean	fix: make `privateToUserNameAux` more robust	2022-09-06 17:15:56 -07:00
prvNameWithMacroScopes.lean.expected.out	fix: make `privateToUserNameAux` more robust	2022-09-06 17:15:56 -07:00
pureCoeIssue.lean
pureCoeIssue.lean.expected.out
rat1.lean
rat1.lean.expected.out
rawStringEOF.lean	feat: Rust-style raw string literals (#2929 )	2023-12-20 16:53:08 +00:00
rawStringEOF.lean.expected.out	feat: Rust-style raw string literals (#2929 )	2023-12-20 16:53:08 +00:00
readDir.lean
readDir.lean.expected.out
reduceBool.lean	chore: add axiom for tracking use of reduceBool / reduceNat (#2654 )	2023-10-11 01:47:59 +00:00
reduceBool.lean.expected.out	chore: add axiom for tracking use of reduceBool / reduceNat (#2654 )	2023-10-11 01:47:59 +00:00
redundantAlt.lean
redundantAlt.lean.expected.out
ref1.lean
ref1.lean.expected.out
refineFiltersOldMVars.lean	fix: only return new mvars from `refine`, `elabTermWithHoles`, and `withCollectingNewGoalsFrom` (#2502 )	2023-09-21 14:23:27 +10:00
refineFiltersOldMVars.lean.expected.out	fix: only return new mvars from `refine`, `elabTermWithHoles`, and `withCollectingNewGoalsFrom` (#2502 )	2023-09-21 14:23:27 +10:00
refineOccursCheck.lean
refineOccursCheck.lean.expected.out
Reformat.lean
Reformat.lean.expected.out	fix: spacing and indentation fixes	2023-05-28 18:48:36 -07:00
renameBug.lean
renameBug.lean.expected.out
renameI.lean
renameI.lean.expected.out
replaceLocalDeclInstantiateMVars.lean	fix: add `instantiateMVars` to `replaceLocalDecl` (#2712 )	2023-10-25 10:26:09 +11:00
replaceLocalDeclInstantiateMVars.lean.expected.out	fix: add `instantiateMVars` to `replaceLocalDecl` (#2712 )	2023-10-25 10:26:09 +11:00
repr.lean
repr.lean.expected.out
repr_issue.lean
repr_issue.lean.expected.out
resolveGlobalName.lean	chore: snake-case attributes (part 1)	2022-10-19 09:28:08 -07:00
resolveGlobalName.lean.expected.out
revertlet.lean
revertlet.lean.expected.out
rewrite.lean	feat: do not instantiate metavariables in kabstract/rw for disallowed occurrences (#2539 )	2024-01-03 00:01:40 +00:00
rewrite.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
rfl_simp_thm.lean
rfl_simp_thm.lean.expected.out
root.lean	feat: enable failIfUnchanged by default in simp	2023-08-16 10:14:23 -07:00
root.lean.expected.out	feat: enable failIfUnchanged by default in simp	2023-08-16 10:14:23 -07:00
run_meta1.lean	fix: `run_meta` macro (#3334 )	2024-02-15 00:12:45 +00:00
run_meta1.lean.expected.out	fix: `run_meta` macro (#3334 )	2024-02-15 00:12:45 +00:00
runSTBug.lean
runSTBug.lean.expected.out
runTacticMustCatchExceptions.lean	feat: improve `runTactic`	2022-07-25 07:41:50 -07:00
runTacticMustCatchExceptions.lean.expected.out	feat: failing macros to show error from first registered rule (#3771 )	2024-03-26 22:24:45 +00:00
rwEqThms.lean
rwEqThms.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
rwPrioritizesLCtxOverEnv.lean	fix: make `rw [foo]` look in the local context for `foo` before it looks in the environment (#2738 )	2023-10-30 14:08:02 +11:00
rwPrioritizesLCtxOverEnv.lean.expected.out	fix: make `rw [foo]` look in the local context for `foo` before it looks in the environment (#2738 )	2023-10-30 14:08:02 +11:00
rwWithoutOffsetCnstrs.lean	feat: dynamic quotations for categories	2022-10-18 14:59:14 -07:00
rwWithoutOffsetCnstrs.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
rwWithSynthesizeBug.lean	fix: `rw ... at h` unknown fvar bug (#2728 )	2023-10-25 01:52:19 +00:00
rwWithSynthesizeBug.lean.expected.out	fix: `rw ... at h` unknown fvar bug (#2728 )	2023-10-25 01:52:19 +00:00
safeShadowing.lean
safeShadowing.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
sanitizeMacroScopes.lean
sanitizeMacroScopes.lean.expected.out	chore: fix tests	2022-08-15 08:55:25 -07:00
sanitychecks.lean
sanitychecks.lean.expected.out	fix: type class issues with `maxSynthPendingDepth := 1` (#4119 )	2024-05-14 03:03:32 +00:00
scientific.lean	test: more unit tests	2022-08-17 05:57:22 -07:00
scientific.lean.expected.out	feat: include unexpected token in error message	2023-09-12 11:42:24 +02:00
scopedInstanceOutsideNamespace.lean
scopedInstanceOutsideNamespace.lean.expected.out
scopedLocalInsts.lean
scopedLocalInsts.lean.expected.out	fix: type class issues with `maxSynthPendingDepth := 1` (#4119 )	2024-05-14 03:03:32 +00:00
scopedMacros.lean
scopedMacros.lean.expected.out	fix: replace uses of token antiquotations for setting position ranges with `withRef`	2022-08-13 18:07:30 -07:00
scopedTokens.lean
scopedTokens.lean.expected.out
scopedunifhint.lean
scopedunifhint.lean.expected.out	chore: remove dangerous instances	2022-12-21 04:24:39 +01:00
semicolonOrLinebreak.lean
semicolonOrLinebreak.lean.expected.out	fix: type class issues with `maxSynthPendingDepth := 1` (#4119 )	2024-05-14 03:03:32 +00:00
sepByIndentQuot.lean
sepByIndentQuot.lean.expected.out	feat: intra-line withPosition formatting	2022-11-28 09:02:08 -08:00
setLit.lean	chore: set literal notation (#3348 )	2024-02-19 23:22:36 +00:00
setLit.lean.expected.out	fix: type class issues with `maxSynthPendingDepth := 1` (#4119 )	2024-05-14 03:03:32 +00:00
shadow.lean
shadow.lean.expected.out	feat: do not generate code for declarations that will be specialized	2022-10-15 08:54:46 -07:00
simp_all_duplicateHyps.lean
simp_all_duplicateHyps.lean.expected.out
simp_dsimp.lean	feat: enable failIfUnchanged by default in simp	2023-08-16 10:14:23 -07:00
simp_dsimp.lean.expected.out
simp_trace.lean	chore: upstream (most of) Std.Data.Nat.Lemmas (#3391 )	2024-02-19 03:47:49 +00:00
simp_trace.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
simp_trace_backtrack.lean	chore: upstream basic statements about inequalities (#3366 )	2024-02-16 05:42:38 +00:00
simp_trace_backtrack.lean.expected.out	chore: upstream basic statements about inequalities (#3366 )	2024-02-16 05:42:38 +00:00
simpArgTypeMismatch.lean
simpArgTypeMismatch.lean.expected.out
simpArrayIdx.lean	feat: port check_tactic commands from Std and add test cases (#3532 )	2024-02-28 23:32:54 +00:00
simpArrayIdx.lean.expected.out	feat: port check_tactic commands from Std and add test cases (#3532 )	2024-02-28 23:32:54 +00:00
simpcfg.lean
simpcfg.lean.expected.out
simpDisch.lean
simpDisch.lean.expected.out	chore: fix tests	2022-08-15 08:55:25 -07:00
simpPrefixIssue.lean
simpPrefixIssue.lean.expected.out
simprocChar.lean	chore: simprocs for Eq	2024-02-17 17:51:24 -08:00
simprocChar.lean.expected.out	chore: simprocs for Eq	2024-02-17 17:51:24 -08:00
simprocEval1.lean	chore: simprocs for Eq	2024-02-17 17:51:24 -08:00
simprocEval1.lean.expected.out	chore: simprocs for Eq	2024-02-17 17:51:24 -08:00
simprocEval2.lean	chore: simprocs for Eq	2024-02-17 17:51:24 -08:00
simprocEval2.lean.expected.out	chore: simprocs for Eq	2024-02-17 17:51:24 -08:00
simprocEval3.lean	chore: simprocs for Eq	2024-02-17 17:51:24 -08:00
simprocEval3.lean.expected.out	chore: simprocs for Eq	2024-02-17 17:51:24 -08:00
simprocEval4.lean	chore: simprocs for Eq	2024-02-17 17:51:24 -08:00
simprocEval4.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
simprocTrace.lean	chore: fix tests	2024-02-01 16:58:54 +11:00
simprocTrace.lean.expected.out	feat: trace `simproc`s	2024-01-09 12:57:15 +01:00
simpTracePostIssue.lean	fix: `simp.trace` missing pre annotation	2024-01-09 12:57:15 +01:00
simpTracePostIssue.lean.expected.out	fix: `simp.trace` missing pre annotation	2024-01-09 12:57:15 +01:00
simpZetaFalse.lean	chore: fix tests	2023-11-09 04:06:30 -08:00
simpZetaFalse.lean.expected.out	fix: do not pretty print theorems with generalized field notation (#3750 )	2024-03-23 09:20:48 +00:00
sizeof.lean	feat: make `#check <ident>` always show the signature without elaboration	2022-12-21 21:59:05 +01:00
sizeof.lean.expected.out	fix: make `delabConstWithSignature` avoid using inaccessible names (#3625 )	2024-03-07 18:14:06 +00:00
smartUnfolding.lean	fix: fixes #1886	2022-11-28 06:50:44 -08:00
smartUnfolding.lean.expected.out	feat: better support for reducing `Nat.rec` (#3616 )	2024-03-06 13:28:07 +00:00
smartUnfoldingMatch.lean
smartUnfoldingMatch.lean.expected.out	fix: Option.getD eagerly evaluates dflt (#3043 )	2023-12-11 10:07:30 +00:00
sorryAtError.lean
sorryAtError.lean.expected.out	feat: extract `delabAppCore`, define `withOverApp`, and make over-applied projections pretty print (#3083 )	2024-01-10 13:24:28 +00:00
sorryWarning.lean
sorryWarning.lean.expected.out
specializeAttr.lean	test: specialize attribute tests	2022-09-07 16:32:25 -07:00
specializeAttr.lean.expected.out	test: specialize attribute tests	2022-09-07 16:32:25 -07:00
splitIssue.lean
splitIssue.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
stdio.lean
stdio.lean.expected.out
stream.lean
stream.lean.expected.out
strictImplicit.lean
strictImplicit.lean.expected.out	feat: make `#check <ident>` always show the signature without elaboration	2022-12-21 21:59:05 +01:00
string_gaps.lean	feat: string gaps for continuing string literals across multiple lines (#2821 )	2023-12-07 08:17:00 +00:00
string_gaps.lean.expected.out	feat: string gaps for continuing string literals across multiple lines (#2821 )	2023-12-07 08:17:00 +00:00
string_gaps_err_newline.lean	feat: string gaps for continuing string literals across multiple lines (#2821 )	2023-12-07 08:17:00 +00:00
string_gaps_err_newline.lean.expected.out	feat: string gaps for continuing string literals across multiple lines (#2821 )	2023-12-07 08:17:00 +00:00
string_imp.lean	fix: `String.splitOn` bug (#3832 )	2024-04-04 09:30:53 +00:00
string_imp.lean.expected.out	fix: `String.splitOn` bug (#3832 )	2024-04-04 09:30:53 +00:00
string_imp2.lean	test: `String.get'` and `String.next'`	2022-11-09 17:02:49 -08:00
string_imp2.lean.expected.out	test: `String.get'` and `String.next'`	2022-11-09 17:02:49 -08:00
struct1.lean	fix: make `elabTermEnsuringType` respect `errToSorry` when there is a type mismatch (#3633 )	2024-03-09 15:30:47 +00:00
struct1.lean.expected.out	fix: `private` + `pp.fullNames`	2022-12-21 21:59:05 +01:00
structAutoBound.lean
structAutoBound.lean.expected.out	feat: `#print` command shows structure fields (#3768 )	2024-04-24 03:18:09 +00:00
structDefault.lean
structDefault.lean.expected.out
structDefValueOverride.lean
structDefValueOverride.lean.expected.out
structInst1.lean	feat: allow multiple source + no expected type	2022-09-13 07:09:08 -07:00
structInst1.lean.expected.out	feat: use signature pretty printer in `#check id`/`#check @id`	2022-12-21 21:59:05 +01:00
structInstError.lean
structInstError.lean.expected.out
structInstExtraEta.lean	feat: flatten parent projections when pretty printing structure instance notation (#3749 )	2024-03-23 09:20:52 +00:00
structInstExtraEta.lean.expected.out	fix: `zetaDelta := false` regression (#3459 )	2024-02-22 19:10:02 +00:00
structInstSourcesLeftToRight.lean	feat: flatten parent projections when pretty printing structure instance notation (#3749 )	2024-03-23 09:20:52 +00:00
structInstSourcesLeftToRight.lean.expected.out	feat: delaboration collapses parent projections (#3326 )	2024-02-14 23:44:48 +00:00
structSorryBug.lean
structSorryBug.lean.expected.out
StxQuot.lean	feat: allow trailing comma in tuples, lists, and tactics (#2643 )	2023-11-17 13:31:41 +01:00
StxQuot.lean.expected.out	chore: fix tests	2024-03-13 21:15:48 -07:00
substBadMotive.lean	feat: per-function termination hints	2024-01-10 17:27:35 +01:00
substBadMotive.lean.expected.out	fix: tests	2023-05-15 09:05:41 -07:00
substFails.lean	feat: subst notation (heq ▸ h) tries both orientation (#4046 )	2024-05-02 07:02:40 +00:00
substFails.lean.expected.out	feat: subst notation (heq ▸ h) tries both orientation (#4046 )	2024-05-02 07:02:40 +00:00
substlet.lean
substlet.lean.expected.out
syntaxErrors.lean
syntaxErrors.lean.expected.out
syntaxInNamespacesAndPP.lean
syntaxInNamespacesAndPP.lean.expected.out	chore: unexpanders for `Name.mkStr` and `Array.mkArray`	2022-10-04 17:18:36 -07:00
syntaxPrec.lean
syntaxPrec.lean.expected.out	feat: include unexpected token in error message	2023-09-12 11:42:24 +02:00
syntheticHolesAsPatterns.lean
syntheticHolesAsPatterns.lean.expected.out	chore: fix tests output	2023-10-22 06:48:22 -07:00
synthorder.lean	feat: reorder tc subgoals according to out-params	2023-04-10 13:00:04 -07:00
synthorder.lean.expected.out	feat: shorten auto-generated instance names (#3089 )	2024-04-13 18:08:50 +00:00
tabulate.lean
tabulate.lean.expected.out
tacUnsolvedGoalsErrors.lean
tacUnsolvedGoalsErrors.lean.expected.out	feat: intra-line withPosition formatting	2022-11-28 09:02:08 -08:00
tcloop.lean
tcloop.lean.expected.out	fix: type class issues with `maxSynthPendingDepth := 1` (#4119 )	2024-05-14 03:03:32 +00:00
termination_by.lean	feat: per-function termination hints	2024-01-10 17:27:35 +01:00
termination_by.lean.expected.out	feat: per-function termination hints	2024-01-10 17:27:35 +01:00
termination_by_vars.lean	feat: improve termination_by error messages (#3255 )	2024-02-05 13:13:53 +00:00
termination_by_vars.lean.expected.out	feat: improve termination_by error messages (#3255 )	2024-02-05 13:13:53 +00:00
termination_by_where.lean	feat: per-function termination hints	2024-01-10 17:27:35 +01:00
termination_by_where.lean.expected.out	feat: per-function termination hints	2024-01-10 17:27:35 +01:00
terminationFailure.lean
terminationFailure.lean.expected.out	fix: make `delabConstWithSignature` avoid using inaccessible names (#3625 )	2024-03-07 18:14:06 +00:00
test_extern.lean	feat: improvements to test_extern command (#3075 )	2024-04-24 03:56:16 +00:00
test_extern.lean.expected.out	feat: improvements to test_extern command (#3075 )	2024-04-24 03:56:16 +00:00
test_single.sh
theoremType.lean
theoremType.lean.expected.out
thunk.lean
thunk.lean.expected.out
toExpr.lean	test: `toExpr` tests	2024-02-23 15:16:12 -08:00
toExpr.lean.expected.out	test: `toExpr` tests	2024-02-23 15:16:12 -08:00
toFieldNameIssue.lean
toFieldNameIssue.lean.expected.out	feat: flatten parent projections when pretty printing structure instance notation (#3749 )	2024-03-23 09:20:52 +00:00
tokenErrors.lean
tokenErrors.lean.expected.out
tooManyVarsAtInduction.lean
tooManyVarsAtInduction.lean.expected.out
traceClassScopes.lean	feat: dynamic quotations for categories	2022-10-18 14:59:14 -07:00
traceClassScopes.lean.expected.out
traceStateBactracking.lean
traceStateBactracking.lean.expected.out
traceTacticSteps.lean
traceTacticSteps.lean.expected.out	feat: use `with_trace` for important trace classes	2023-04-10 16:57:54 +02:00
trailingComma.lean	feat: allow trailing comma in tuples, lists, and tactics (#2643 )	2023-11-17 13:31:41 +01:00
trailingComma.lean.expected.out	feat: allow trailing comma in tuples, lists, and tactics (#2643 )	2023-11-17 13:31:41 +01:00
treeMap.lean	feat: per-function termination hints	2024-01-10 17:27:35 +01:00
treeMap.lean.expected.out	fix: Fix/GuessLex: refine through more casesOnApp/matcherApp (#3176 )	2024-01-13 18:02:41 +00:00
typeIncorrectPat.lean
typeIncorrectPat.lean.expected.out
typeMismatch.lean
typeMismatch.lean.expected.out
typeOf.lean
typeOf.lean.expected.out	fix: type class issues with `maxSynthPendingDepth := 1` (#4119 )	2024-05-14 03:03:32 +00:00
uintCtors.lean
uintCtors.lean.expected.out
uintMatch.lean
uintMatch.lean.expected.out
unboxStruct.lean
unboxStruct.lean.expected.out
unexpander.lean	chore: snake-case attributes (part 1)	2022-10-19 09:28:08 -07:00
unexpander.lean.expected.out
unexpandersNamespaces.lean
unexpandersNamespaces.lean.expected.out
UnexpandSubtype.lean
UnexpandSubtype.lean.expected.out
unfold1.lean	feat: per-function termination hints	2024-01-10 17:27:35 +01:00
unfold1.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
unfoldDefEq.lean
unfoldDefEq.lean.expected.out
unfoldFailure.lean
unfoldFailure.lean.expected.out
unfoldReduceMatch.lean
unfoldReduceMatch.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
unhygienic.lean
unhygienic.lean.expected.out
unhygienicCode.lean	chore: default `compiler.enableNew` to false until development restarts (#3034 )	2023-12-21 07:48:25 +00:00
unhygienicCode.lean.expected.out	chore: default `compiler.enableNew` to false until development restarts (#3034 )	2023-12-21 07:48:25 +00:00
unifHintAndTC.lean
unifHintAndTC.lean.expected.out	fix: make tests be aware of new instance names (#3936 )	2024-04-17 16:14:51 +02:00
univInference.lean
univInference.lean.expected.out	doc: fix typos around inductiveCheckResultingUniverse (#3309 )	2024-02-12 10:11:50 +00:00
unknownId.lean
unknownId.lean.expected.out
unknownTactic.lean
unknownTactic.lean.expected.out	chore: fix tests	2022-10-11 17:24:35 -07:00
unnecessaryUnfolding.lean
unnecessaryUnfolding.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
unsolvedIndCases.lean
unsolvedIndCases.lean.expected.out	feat: custom eliminators for `induction` and `cases` tactics, and beautiful eliminators for `Nat` (#3629 )	2024-03-09 15:31:51 +00:00
unsound.lean
unsound.lean.expected.out
unused_univ.lean
unused_univ.lean.expected.out
unusedLet.lean
unusedLet.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
unusedWarningAtStructUpdate.lean	feat: add missingDocs linter	2022-07-31 18:18:21 -07:00
unusedWarningAtStructUpdate.lean.expected.out
updateExprIssue.lean
updateExprIssue.lean.expected.out
updateLevelIssues.lean
updateLevelIssues.lean.expected.out
Uri.lean	chore: move Bootstrap.System.Uri to Init	2022-08-29 08:06:30 -07:00
Uri.lean.expected.out	chore: use new comment syntax	2022-09-14 08:26:17 -07:00
varBinderUpdate.lean	feat: make `#check <ident>` always show the signature without elaboration	2022-12-21 21:59:05 +01:00
varBinderUpdate.lean.expected.out	fix: make `delabConstWithSignature` avoid using inaccessible names (#3625 )	2024-03-07 18:14:06 +00:00
warningAsError.lean	feat: add `linter.deprecated` option to silence deprecation warnings	2022-10-23 21:11:57 +02:00
warningAsError.lean.expected.out	feat: make linter options more explicitly discoverable (#3938 )	2024-04-18 07:20:55 +00:00
wf1.lean
wf1.lean.expected.out	feat: infer termination arguments like `xs.size - i` (#3666 )	2024-03-16 12:27:35 +00:00
wf2.lean	feat: per-function termination hints	2024-01-10 17:27:35 +01:00
wf2.lean.expected.out	chore: fix tests	2022-10-11 17:24:35 -07:00
wfrecUnusedLet.lean	feat: drop support for termination_by' (#3033 )	2023-12-11 17:33:17 +00:00
wfrecUnusedLet.lean.expected.out	feat: well-founded definitions irreducible by default (#4061 )	2024-05-10 06:45:21 +00:00
whnfProj.lean
whnfProj.lean.expected.out	feat: enable `pp.fieldNotation.generalized` globally (#3744 )	2024-03-23 02:38:09 +00:00
wildcardAlt.lean
wildcardAlt.lean.expected.out
withAssignableSyntheticOpaqueBug.lean
withAssignableSyntheticOpaqueBug.lean.expected.out
withLocation.lean	fix: withLocation should use withMainContext for target (#2607 )	2023-10-04 10:12:43 +11:00
withLocation.lean.expected.out	fix: withLocation should use withMainContext for target (#2607 )	2023-10-04 10:12:43 +11:00
withLocationImplementationDetails.lean	fix: ignore implDetail hyps in withLocation	2023-05-28 17:40:55 -07:00
withLocationImplementationDetails.lean.expected.out	fix: ignore implDetail hyps in withLocation	2023-05-28 17:40:55 -07:00
withSetOptionIn.lean	fix: typo in `withSetOptionIn` (#3806 )	2024-04-06 18:00:34 +00:00
withSetOptionIn.lean.expected.out	fix: typo in `withSetOptionIn` (#3806 )	2024-04-06 18:00:34 +00:00
workspaceSymbols.lean	fix: fuzzy-find bonus for matching last characters of pattern and symbol (#1917 )	2023-01-19 09:06:53 +01:00
workspaceSymbols.lean.expected.out	fix: fuzzy-find bonus for matching last characters of pattern and symbol (#1917 )	2023-01-19 09:06:53 +01:00
xmlParsing.lean	fix: XML parsing bugs (#2601 )	2023-10-04 11:51:22 +11:00
xmlParsing.lean.expected.out	fix: XML parsing bugs (#2601 )	2023-10-04 11:51:22 +11:00
zipper.lean
zipper.lean.expected.out