max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Lean/Meta/Tactic
History
Kyle Miller 36c2511b27
feat: options pp.mvars.anonymous and pp.mvars.levels (#5711) 
Gives more control over pretty printing metavariables.

- When `pp.mvars.levels` is false, then universe level metavariables
pretty print as `_` rather than `?u.22`
- When `pp.mvars.anonymous` is false, then anonymous metavariables
pretty print as `?_` rather than `?m.22`. Named metavariables still
pretty print with their names. When this is false, it also sets
`pp.mvars.levels` to false, since every level metavariable is anonymous.
- When `pp.mvars` is false, then all metavariables pretty print as `?_`
or `_`.

Modifies TryThis to use `pp.mvars.anonymous` rather than doing a
post-delaboration modification. This incidentally improves TryThis since
it now prints universe level metavariables as `_` rather than `?u.22`.
2024-10-14 21:44:15 +00:00
..
AC feat: support at in ac_nf and use it in bv_normalize (#5618) 2024-10-07 11:37:17 +00:00
Grind chore: fix spelling mistakes in src/Lean/Meta/ (#5436) 2024-09-23 23:09:14 +00:00
LinearArith perf: use with_reducible in special-purpose decreasing_trivial macros (#3991) 2024-04-29 15:12:27 +00:00
Simp chore: fix spelling mistakes (#5599) 2024-10-02 21:32:22 +00:00
AC.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Acyclic.lean fix: regression on match expressions with builtin literals (#3521) 2024-02-27 18:49:44 +00:00
Apply.lean chore: cleanup after export Bool.and/or/not/xor 2024-09-16 12:45:51 +10:00
Assert.lean feat: allow MVarId.assertHypotheses to set BinderInfo/Kind (#5587) 2024-10-02 05:09:49 +00:00
Assumption.lean chore: delete deprecations from 2022 (#4618) 2024-07-02 03:47:33 +00:00
AuxLemma.lean feat: propagate maxHeartbeats to kernel (#4113) 2024-05-09 17:44:19 +00:00
Backtrack.lean chore: rename List.join to List.flatten 2024-10-14 22:28:12 +11:00
Cases.lean chore: fix spelling mistakes in src/Lean/Meta/ (#5436) 2024-09-23 23:09:14 +00:00
Cleanup.lean chore: delete deprecations from 2022 (#4618) 2024-07-02 03:47:33 +00:00
Clear.lean feat: variant of MVarId.tryClearMany (#5588) 2024-10-02 05:26:40 +00:00
Congr.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Constructor.lean chore: delete deprecations from 2022 (#4618) 2024-07-02 03:47:33 +00:00
Contradiction.lean chore: delete deprecations from 2022 (#4618) 2024-07-02 03:47:33 +00:00
Delta.lean chore: delete deprecations from 2022 (#4618) 2024-07-02 03:47:33 +00:00
ElimInfo.lean refactor: more idiomatic syntax for if h: (#5567) 2024-10-01 15:23:54 +00:00
FunInd.lean fix: FunInd: avoid over-eta-expanding in preprocessing step (#5619) 2024-10-07 19:47:43 +00:00
FVarSubst.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Generalize.lean chore: update copyrights (#5449) 2024-09-24 05:27:53 +00:00
Grind.lean feat: add grind core module (#4249) 2024-05-22 03:50:36 +00:00
IndependentOf.lean chore: upstream solve_by_elim (#3408) 2024-02-21 01:16:04 +00:00
Induction.lean chore: delete deprecations from 2022 (#4618) 2024-07-02 03:47:33 +00:00
Injection.lean fix: regression on match expressions with builtin literals (#3521) 2024-02-27 18:49:44 +00:00
Intro.lean chore: remove repeated words (#5438) 2024-09-24 03:40:11 +00:00
LibrarySearch.lean chore: update copyrights (#5449) 2024-09-24 05:27:53 +00:00
LinearArith.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
NormCast.lean feat: use attribute command to add and erase simprocs (#3511) 2024-02-26 23:41:49 +00:00
Refl.lean feat: apply_rfl tactic: handle Eq, HEq, better error messages (#3714) 2024-09-20 08:25:10 +00:00
Rename.lean chore: delete deprecations from 2022 (#4618) 2024-07-02 03:47:33 +00:00
Repeat.lean chore: update copyrights (#5449) 2024-09-24 05:27:53 +00:00
Replace.lean chore: remove >6 month deprecations (#5199) 2024-08-29 05:18:44 +00:00
Revert.lean chore: delete deprecations from 2022 (#4618) 2024-07-02 03:47:33 +00:00
Rewrite.lean chore: cleanup after export Bool.and/or/not/xor 2024-09-16 12:45:51 +10:00
Rewrites.lean chore: update copyrights (#5449) 2024-09-24 05:27:53 +00:00
Rfl.lean refactor: back rfl tactic primarily via apply_rfl (#3718) 2024-09-25 10:34:42 +00:00
Simp.lean feat: report diagnostic information for simp at exception 2024-05-01 03:19:39 +02:00
SolveByElim.lean chore: update copyrights (#5449) 2024-09-24 05:27:53 +00:00
Split.lean fix: improve split discriminant generalization strategy (#4401) 2024-06-07 21:35:09 +00:00
SplitIf.lean fix: split (for if-expressions) should work on non-propositional goals (#4349) 2024-06-05 04:43:46 +00:00
Subst.lean chore: fix spelling mistakes in src/Lean/Meta/ (#5436) 2024-09-23 23:09:14 +00:00
Symm.lean chore: update copyrights (#5449) 2024-09-24 05:27:53 +00:00
TryThis.lean feat: options pp.mvars.anonymous and pp.mvars.levels (#5711) 2024-10-14 21:44:15 +00:00
Unfold.lean feat: let unfold do zeta-delta reduction of local definitions (#4834) 2024-09-07 21:48:08 +00:00
UnifyEq.lean fix: missing withIncRecDepth and unifyEqs? and add support for offsets at unifyEq? (#4224) 2024-05-20 13:42:36 +00:00
Util.lean chore: delete deprecations from 2022 (#4618) 2024-07-02 03:47:33 +00:00