max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Lean/Elab
History
Marc Huisinga 3930100b67
feat: whitespace tactic completion & tactic completion docs (#5666) 
This PR enables tactic completion in the whitespace of a tactic proof
and adds tactic docstrings to the completion menu.

Future work:
- A couple of broken tactic completions: This is due to tactic
completion now using @david-christiansen's `Tactic.Doc.allTacticDocs` to
obtain the tactic docstrings and should be fixed soon.
- Whitespace tactic completion in tactic combinators: This requires
changing the syntax of tactic combinators to produce a syntax node that
makes it clear that a tactic is expected at the given position.

Closes #1651.
2024-10-10 13:28:34 +00:00
..
Deriving refactor: more idiomatic syntax for if h: (#5567) 2024-10-01 15:23:54 +00:00
InfoTree feat: whitespace tactic completion & tactic completion docs (#5666) 2024-10-10 13:28:34 +00:00
PreDefinition refactor: more idiomatic syntax for if h: (#5567) 2024-10-01 15:23:54 +00:00
Quotation feat: reserved names (#3675) 2024-03-15 00:33:22 +00:00
Tactic feat: whitespace tactic completion & tactic completion docs (#5666) 2024-10-10 13:28:34 +00:00
App.lean feat: allow explicit mode with field notation (#5528) 2024-10-09 07:03:46 +00:00
Arg.lean feat: actual implementation for #5283 (#5512) 2024-09-29 01:22:12 +00:00
Attributes.lean chore: fix linter errors (#4502) 2024-06-19 18:24:08 +00:00
AutoBound.lean doc: fix option name (#5150) 2024-08-25 07:16:44 +00:00
AuxDef.lean chore: fix spelling mistakes in src/Lean/Elab/ (#5435) 2024-09-23 21:58:16 +00:00
BinderPredicates.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Binders.lean feat: localize universe metavariable errors at let bindings and fun binders (#5402) 2024-09-24 05:30:42 +00:00
BindersUtil.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
BuiltinCommand.lean feat: better #eval command (#5627) 2024-10-08 20:51:46 +00:00
BuiltinEvalCommand.lean feat: better #eval command (#5627) 2024-10-08 20:51:46 +00:00
BuiltinNotation.lean refactor: more idiomatic syntax for if h: (#5567) 2024-10-01 15:23:54 +00:00
BuiltinTerm.lean feat: have autoparams report parameter/field on failure (#5474) 2024-09-27 19:00:59 +00:00
Calc.lean fix: make "use `set_option diagnostics true" message conditional on current setting (#4781) 2024-07-31 03:53:09 +00:00
CheckTactic.lean chore: missing withSynthesize in #check_tactic (#4489) 2024-06-18 05:24:45 +00:00
Command.lean feat: better #eval command (#5627) 2024-10-08 20:51:46 +00:00
ComputedFields.lean refactor: Split Constructions module (#4656) 2024-07-05 08:25:44 +00:00
Config.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Declaration.lean fix: call hierarchy into (builtin_)initialize (#5560) 2024-10-03 12:03:44 +00:00
DeclarationRange.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
DeclModifiers.lean chore: fix spelling mistakes in src/Lean/Elab/ (#5435) 2024-09-23 21:58:16 +00:00
DeclNameGen.lean refactor: more idiomatic syntax for if h: (#5567) 2024-10-01 15:23:54 +00:00
DeclUtil.lean feat: localize universe metavariable errors at let bindings and fun binders (#5402) 2024-09-24 05:30:42 +00:00
DefView.lean fix: [implemented_by] at functions defined by well-founded recursion (#4508) 2024-06-20 00:06:38 +00:00
Deriving.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Do.lean refactor: more idiomatic syntax for if h: (#5567) 2024-10-01 15:23:54 +00:00
ElabRules.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Eval.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Exception.lean feat: incremental elaboration of definition headers, bodies, and tactics (#3940) 2024-05-22 13:23:30 +00:00
Extra.lean chore: remove repeated words (#5438) 2024-09-24 03:40:11 +00:00
Frontend.lean chore: clean up cmdline snapshots logic (#5043) 2024-08-14 15:10:37 +00:00
GenInjective.lean feat: reserved names (#3675) 2024-03-15 00:33:22 +00:00
GuardMsgs.lean fix: now linters in general do not run on #guard_msgs itself (#5644) 2024-10-08 17:35:07 +00:00
Import.lean chore: revert "fix: make import resolution case-sensitive on all platforms" (#4896) 2024-08-01 13:55:37 +00:00
Inductive.lean feat: infer Prop for inductive/structure when defining syntactic subsingletons (#5517) 2024-10-08 22:39:38 +00:00
InfoTree.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
InheritDoc.lean feat: @[builtin_doc] attribute (part 2) (#3918) 2024-09-13 08:05:10 +00:00
LetRec.lean feat: termination_by structural (#4542) 2024-07-01 16:51:30 +00:00
Level.lean fix: mutual inductives with instance parameters (#4342) 2024-06-04 17:35:41 +00:00
Macro.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
MacroArgUtil.lean feat: quotations for parser aliases (#4307) 2024-05-30 09:22:22 +00:00
MacroRules.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Match.lean refactor: more idiomatic syntax for if h: (#5567) 2024-10-01 15:23:54 +00:00
MatchAltView.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
MatchExpr.lean perf: match_expr join points (#3580) 2024-03-03 18:15:49 +00:00
Mixfix.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
MutualDef.lean refactor: more idiomatic syntax for if h: (#5567) 2024-10-01 15:23:54 +00:00
Notation.lean feat: apply app unexpanders for all prefixes of an application (#3375) 2024-02-27 07:04:17 +00:00
Open.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
ParseImportsFast.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
PatternVar.lean chore: make Array functions either semireducible or use structural recursion (#5420) 2024-09-23 02:41:41 +00:00
PreDefinition.lean feat: generate f.eq_unfold lemmas (#5141) 2024-08-29 16:47:40 +00:00
Print.lean feat: fine-grained equational lemmas for non-recursive functions (#4154) 2024-08-22 13:26:58 +00:00
Quotation.lean refactor: more idiomatic syntax for if h: (#5567) 2024-10-01 15:23:54 +00:00
RecAppSyntax.lean chore: fix spelling mistakes in src/Lean/Elab/ (#5435) 2024-09-23 21:58:16 +00:00
SetOption.lean fix: don't use info nodes before cursor for completion (#3778) 2024-04-02 08:49:24 +00:00
StructInst.lean feat: allow explicit mode with field notation (#5528) 2024-10-09 07:03:46 +00:00
Structure.lean feat: infer Prop for inductive/structure when defining syntactic subsingletons (#5517) 2024-10-08 22:39:38 +00:00
Syntax.lean chore: missing registerTraceClass (#4369) 2024-06-06 00:53:16 +00:00
SyntheticMVars.lean refactor: more idiomatic syntax for if h: (#5567) 2024-10-01 15:23:54 +00:00
Tactic.lean feat: add BitVec.intMin 2024-08-27 11:26:16 +10:00
Term.lean fix: store local context for 'don't know how to synthesize implicit argument' errors (#5658) 2024-10-09 08:40:21 +00:00
Time.lean chore: upstream #time command (#5044) 2024-08-15 00:17:48 +00:00
Util.lean feat: simp to still work even if one simp arg does not work (#4177) 2024-06-03 14:21:31 +00:00