Zulip Chat Archive

Stream: metaprogramming / tactics

---

Topics:

• dependent rewrite tactic (19 messages, latest: Apr 29 2025 at 01:49)
• ✔ Aesop TacGen with arguments (5 messages, latest: Apr 28 2025 at 22:45)
• More granular binder info control in mkForallFvars (4 messages, latest: Apr 28 2025 at 15:39)
• mvars left in types after mkForallFVars (11 messages, latest: Apr 28 2025 at 12:24)
• detect termination proof obligations in TacticM (2 messages, latest: Apr 19 2025 at 20:01)
• ✔ Differentiate def and theorem (4 messages, latest: Apr 19 2025 at 19:20)
• proof->ast->proof (22 messages, latest: Apr 18 2025 at 20:22)
• tree structure from a proof (15 messages, latest: Apr 16 2025 at 23:44)
• ✔ how to get related theorems (11 messages, latest: Apr 16 2025 at 17:44)
• ✔ Generating computable code (6 messages, latest: Apr 15 2025 at 21:58)
• noWs (20 messages, latest: Apr 15 2025 at 18:30)
• mutual induction tactic (50 messages, latest: Apr 11 2025 at 14:25)
• Intended way to add local declaration to local context (32 messages, latest: Apr 08 2025 at 03:12)
• Synthesize a type from instance binder in tactic (24 messages, latest: Apr 06 2025 at 23:18)
• Change elaboration of example (49 messages, latest: Apr 05 2025 at 17:52)
• matching on syntax alternatives (5 messages, latest: Apr 04 2025 at 10:22)
• ✔ Difference between two LCtx (12 messages, latest: Apr 03 2025 at 11:38)
• syntax quotation and matching (13 messages, latest: Apr 02 2025 at 11:14)
• Collecting binders (8 messages, latest: Mar 31 2025 at 19:11)
• ✔ Checking interruption (3 messages, latest: Mar 30 2025 at 02:47)
• ✔ Expansion data in .mdata (8 messages, latest: Mar 17 2025 at 20:05)
• removing an unused typeclass (18 messages, latest: Mar 17 2025 at 03:33)
• change / show changes binder name to x (7 messages, latest: Mar 16 2025 at 23:15)
• checking if two Exprs are defeq (9 messages, latest: Mar 16 2025 at 22:40)
• Tactic that survives the goal it's called on (19 messages, latest: Mar 11 2025 at 00:46)
• isProjectionFn for propositional fields (5 messages, latest: Mar 10 2025 at 01:07)
• guard_target in syntactic mode (14 messages, latest: Mar 06 2025 at 04:27)
• ✔ deduplicating identical goals (7 messages, latest: Mar 05 2025 at 21:59)
• Basic Qq help - matching against both goal and hypothesis (5 messages, latest: Mar 05 2025 at 12:12)
• ✔ access changed local context (4 messages, latest: Mar 04 2025 at 14:17)
• ✔ TSyntax conversion in tactic elab (19 messages, latest: Mar 04 2025 at 08:56)
• ✔ Generating fresh names for universe levels (7 messages, latest: Feb 28 2025 at 08:34)
• run meta program from command line (3 messages, latest: Feb 26 2025 at 10:59)
• ✔ How to extract Type from Expr (6 messages, latest: Feb 21 2025 at 16:56)
• Automatic insertion of show tactic for VSCode? (3 messages, latest: Feb 20 2025 at 08:57)
• MVarId.apply without infering instance arguments (1 message, latest: Feb 18 2025 at 17:43)
• ✔ "maximum recursion depth has been reached" not catchable? (9 messages, latest: Feb 17 2025 at 08:48)
• Tactics as programs in the core type theory? (2 messages, latest: Feb 14 2025 at 21:31)
• ✔ Render Widget from CommandElabM (4 messages, latest: Feb 08 2025 at 02:11)
• adding a new declaration (3 messages, latest: Feb 04 2025 at 18:26)
• ring and ∑ (5 messages, latest: Feb 03 2025 at 18:45)
• ✔ simp? in conv (4 messages, latest: Feb 03 2025 at 02:43)
• Qq doesn't specialize expression with inferred type (1 message, latest: Feb 03 2025 at 02:21)
• using Lean.TSyntax.replaceM to replace a hole in a type (4 messages, latest: Jan 30 2025 at 17:23)
• ✔ Writing recursive elaborators (12 messages, latest: Jan 29 2025 at 04:35)
• Execute headBeta on all local decl (10 messages, latest: Jan 27 2025 at 20:13)
• whnf variant which preserves let-bindings (27 messages, latest: Jan 25 2025 at 17:08)
• Quotient-like match pattern (4 messages, latest: Jan 25 2025 at 04:52)
• Leveraging Lean's macro/elab for String parsing? (6 messages, latest: Jan 23 2025 at 23:01)
• How can I fix "'antiquot' has not been implemented"? (10 messages, latest: Jan 22 2025 at 07:14)
• ✔ Why doesn't this quotation work? (8 messages, latest: Jan 22 2025 at 07:12)
• citing Metaprogramming in Lean 4 (6 messages, latest: Jan 21 2025 at 11:27)
• Introspecting environment extensions (3 messages, latest: Jan 16 2025 at 21:31)
• Examples on delaborating for whitespace/indentation (13 messages, latest: Jan 16 2025 at 18:58)
• hint tactic (5 messages, latest: Jan 13 2025 at 06:08)
• parsing a DSL (36 messages, latest: Jan 11 2025 at 22:20)
• Manual derecursification of PreDefinition (10 messages, latest: Jan 11 2025 at 20:30)
• Converting polynomials to Expr (4 messages, latest: Jan 11 2025 at 19:09)
• False negatives in PtrSet.contains (4 messages, latest: Jan 10 2025 at 10:47)
• Incremental compilation for classical (3 messages, latest: Jan 08 2025 at 12:52)
• presence of decl in env.constants of InfoTree of decl (2 messages, latest: Jan 08 2025 at 12:17)
• omega doesn’t know Even or Odd (2 messages, latest: Jan 08 2025 at 04:26)
• Printing multiple commands using Try this (2 messages, latest: Jan 06 2025 at 09:07)
• Declare types programmatically, via elaborators (12 messages, latest: Jan 05 2025 at 16:38)
• Does anyone have an example of a LetRecToLift? (1 message, latest: Jan 05 2025 at 16:12)
• Can DSLs avoid collision with keywords ? (3 messages, latest: Jan 05 2025 at 09:53)
• ✔ Syntax value corresponding to a def declaration in MetaM (2 messages, latest: Jan 05 2025 at 05:44)
• Prototyping a programming language with Lean4's elaborators (10 messages, latest: Jan 01 2025 at 18:35)
• Best way to write proof automation? (8 messages, latest: Dec 30 2024 at 19:58)
• How to call a simp lemma within a simproc? (2 messages, latest: Dec 30 2024 at 09:30)
• ✔ Help writing a "group rewrite" tactic (6 messages, latest: Dec 21 2024 at 18:17)
• LocalDecl not recognized in MVar (16 messages, latest: Dec 21 2024 at 02:18)
• Clear ._hyg in .mvarId!.getType (6 messages, latest: Dec 20 2024 at 19:39)
• Simulating the scope of an inductive declaration in MetaM (6 messages, latest: Dec 17 2024 at 21:32)
• ✔ How to create term representing a TSyntax? (6 messages, latest: Dec 10 2024 at 04:28)
• exact Generates New MVars w/o Adding Them to the Goal List (2 messages, latest: Dec 05 2024 at 07:20)
• confidence sorry implementation help (30 messages, latest: Dec 05 2024 at 05:29)
• How is TacticM lifted to TermElabM? (10 messages, latest: Dec 03 2024 at 16:10)
• General quotation mechanism to convert a term into Expr (43 messages, latest: Dec 01 2024 at 08:53)
• Help with writing tactic setm (23 messages, latest: Nov 28 2024 at 04:58)
• Using syntax with functions to declare literals (2 messages, latest: Nov 25 2024 at 23:25)
• elaboration-based wrapper around structure (4 messages, latest: Nov 24 2024 at 09:34)
• Inserting Expr into command syntax (1 message, latest: Nov 23 2024 at 18:42)
• Differentiating between tactic and term elaborators (43 messages, latest: Nov 22 2024 at 23:28)
• ✔ generating theorem strings from inductive types (7 messages, latest: Nov 20 2024 at 22:54)
• Roundtripping delaboration involving coercions (7 messages, latest: Nov 18 2024 at 14:09)
• isDefEq variant which preserves let-bindings (55 messages, latest: Nov 16 2024 at 00:11)
• whnf and equation compiler (12 messages, latest: Nov 15 2024 at 19:58)
• Lift from Option to MetaM (16 messages, latest: Nov 09 2024 at 20:46)
• addMorphismPropertyInstances (1 message, latest: Nov 09 2024 at 08:45)
• Incorrect macro expansion(?) in doElem macro (5 messages, latest: Nov 07 2024 at 21:03)
• New config syntax (7 messages, latest: Nov 04 2024 at 20:51)
• Idiom to check whether monad runs without error? (4 messages, latest: Nov 03 2024 at 00:23)
• Calling finiteness in meta code (11 messages, latest: Nov 02 2024 at 12:14)
• Extract and instantiate metavariables of a type (16 messages, latest: Nov 01 2024 at 23:40)
• Tactic to convert logical propositions into DNF (3 messages, latest: Oct 30 2024 at 19:03)
• ✔ typeclass instance problem is stuck with macro (7 messages, latest: Oct 29 2024 at 12:25)
• How do I interact with MetaM within a proof? (4 messages, latest: Oct 26 2024 at 20:12)
• ✔ Difference between Tactic.run and actually running tactic (16 messages, latest: Oct 23 2024 at 03:32)
• Calling CommandElabM from MetaM (3 messages, latest: Oct 22 2024 at 20:26)
• ✔ metaprogramming book DSL issue (3 messages, latest: Oct 19 2024 at 17:08)
• Difference in behavior between performing Tactic.run and act (1 message, latest: Oct 17 2024 at 15:21)
• superfluous proof_1 items in docgen (11 messages, latest: Oct 16 2024 at 12:38)
• proj to const (1 message, latest: Oct 16 2024 at 06:02)
• How to work with clauses efficiently (10 messages, latest: Oct 16 2024 at 05:39)
• Tactic Monad Definition (5 messages, latest: Oct 15 2024 at 01:29)
• Modify declaration in place (48 messages, latest: Oct 14 2024 at 21:37)
• Allow docstring for command (5 messages, latest: Oct 05 2024 at 14:25)
• comparing declarations across environments (32 messages, latest: Oct 04 2024 at 16:12)
• ✔ Storing data between commands (10 messages, latest: Oct 04 2024 at 13:51)
• all_goals + apply elaboration = lost errors (14 messages, latest: Oct 03 2024 at 11:29)
• Generating new inductives from existing (5 messages, latest: Oct 03 2024 at 06:46)
• ✔ Small error disambiguating macro (15 messages, latest: Oct 02 2024 at 09:21)
• "Metaprogramming in Lean 4" (45 messages, latest: Sep 29 2024 at 14:57)
• ✔ How to create a "have" tactic from an Expr? (15 messages, latest: Sep 29 2024 at 13:50)
• ✔ Free variables returned by "Lean.MVarId.intro" (5 messages, latest: Sep 16 2024 at 08:50)
• Exclude private as implementation detail (2 messages, latest: Sep 12 2024 at 04:03)
• An interval tactic for constant real inequalities (22 messages, latest: Sep 08 2024 at 16:09)
• RefinedDiscrTree incompleteness (9 messages, latest: Sep 06 2024 at 16:14)
• Counting declarations (38 messages, latest: Sep 02 2024 at 12:57)
• Version of mkLambdaFVars taking an array of binderinfos (6 messages, latest: Aug 26 2024 at 16:59)
• Specializing function at unknown point (and univese issues) (13 messages, latest: Aug 26 2024 at 15:19)
• Find points in a definition with a particular type (7 messages, latest: Aug 21 2024 at 20:09)
• Using BinderView and toBinderViews (3 messages, latest: Aug 21 2024 at 13:12)
• ✔ Metavariable in type-class for OfNat Nat (8 messages, latest: Aug 14 2024 at 16:28)
• Confused by Metavariable occurance (5 messages, latest: Aug 12 2024 at 10:20)
• solve_by_elim : "only"weirdness (14 messages, latest: Aug 11 2024 at 08:19)
• ✔ Recursive rcases tactic (8 messages, latest: Aug 09 2024 at 19:24)
• Normalizing binder parses (6 messages, latest: Aug 05 2024 at 03:15)
• Compiling a definition to LCNF (2 messages, latest: Jul 29 2024 at 20:51)
• Tactics for Sudoku (2 messages, latest: Jul 29 2024 at 20:46)
• ✔ suffixes of hygienic goals name (11 messages, latest: Jul 26 2024 at 16:41)
• ✔ Errors in manual induction (3 messages, latest: Jul 23 2024 at 19:06)
• ✔ Simp wrapper macro (7 messages, latest: Jul 22 2024 at 19:44)
• Aesop safe apply not triggering (7 messages, latest: Jul 16 2024 at 21:19)
• isBoundedDefault not triggering (8 messages, latest: Jul 10 2024 at 19:39)
• ✔ convert_to at / non-definitional change (4 messages, latest: Jun 29 2024 at 11:05)
• Monoidal category tactics (3 messages, latest: Jun 25 2024 at 01:24)
• Proving sharp inequalities using interval arithmetic (4 messages, latest: Jun 24 2024 at 13:57)
• "case split" for notation/macro? (16 messages, latest: Jun 22 2024 at 17:25)
• channel events (1 message, latest: Jun 21 2024 at 01:34)
• How do I invoke native_decide programmatically? (17 messages, latest: Jun 18 2024 at 20:43)
• Cryptic "unknown constant" error when using syntax extension (14 messages, latest: Jun 13 2024 at 15:30)
• interpolating localDecls into syntax quotations (3 messages, latest: Jun 06 2024 at 15:41)
• Tactic wishlist: Abel (7 messages, latest: Jun 01 2024 at 11:52)
• Testing if tactics work (8 messages, latest: May 29 2024 at 08:38)
• Get current InfoTree (2 messages, latest: May 27 2024 at 17:10)
• modifying local context in MetaM (4 messages, latest: May 27 2024 at 16:18)
• constructing expressions (9 messages, latest: May 23 2024 at 15:31)
• Jump to definition from a widget (14 messages, latest: May 17 2024 at 19:41)
• ✔ omega on defeq hypothesis (5 messages, latest: May 17 2024 at 00:24)
• RPowSimp tactic questions (7 messages, latest: May 16 2024 at 19:34)
• Consolidating duplicate goals (9 messages, latest: May 14 2024 at 09:14)
• ✔ Help understanding failing to create testable instance (5 messages, latest: May 04 2024 at 22:11)
• ✔ Wishlist: Supporting fact in slim_check (3 messages, latest: May 01 2024 at 07:50)
• "try this" suggestion from aesop? fails (2 messages, latest: Apr 30 2024 at 17:14)
• Pretty printing free variables (4 messages, latest: Apr 19 2024 at 05:02)
• Controlling forallTelescope (16 messages, latest: Apr 16 2024 at 17:50)
• positivity discharger (9 messages, latest: Apr 16 2024 at 06:52)
• dsimp in elab_rule? (10 messages, latest: Apr 15 2024 at 04:07)
• ✔ Try elab, else throwUnsupportedSyntax? (6 messages, latest: Apr 15 2024 at 00:14)
• Consume let (6 messages, latest: Apr 12 2024 at 21:50)
• aesop config: assumption multiplies goals? (6 messages, latest: Apr 10 2024 at 12:15)
• Entries from all modules of persistent env extension (23 messages, latest: Apr 03 2024 at 18:23)
• Tactic wishlist: Omega (2 messages, latest: Apr 03 2024 at 09:49)
• Tauto infinite loop (75 messages, latest: Apr 02 2024 at 15:32)
• Persisting hypotheses across tactics (21 messages, latest: Mar 27 2024 at 19:16)
• Metaprogram that evaluates a function from the env (26 messages, latest: Mar 21 2024 at 21:35)
• How to turn a macro_rules into an elab (6 messages, latest: Mar 21 2024 at 14:53)
• Parenthesizing in new notation (9 messages, latest: Mar 18 2024 at 07:11)
• theorems/tactic script used by aesop_cat_nonterminal (8 messages, latest: Mar 15 2024 at 10:25)
• Different error message for copied tactic (1 message, latest: Mar 15 2024 at 09:22)
• Handling associativity when rewriting expressions (5 messages, latest: Mar 12 2024 at 21:47)
• ✔ Writing an "extracting" parser (12 messages, latest: Mar 12 2024 at 07:29)
• ✔ Enter text into the editor given InteractiveGoal (11 messages, latest: Mar 12 2024 at 02:37)
• Implementing sequential composition of program specs (4 messages, latest: Mar 11 2024 at 19:32)
• DiscrTree-accelerated pattern matching (4 messages, latest: Mar 09 2024 at 14:23)
• Distinguishing Type from Prop (29 messages, latest: Mar 05 2024 at 04:04)
• Aesop.buildGlobalRule now needs goal : MVarId (4 messages, latest: Mar 04 2024 at 14:25)
• Idiomatically adding extra hypotheses to Aesop (32 messages, latest: Mar 04 2024 at 09:26)
• Trouble writing a parser involving atoms (19 messages, latest: Mar 02 2024 at 18:33)
• Adding comments to commands (6 messages, latest: Feb 24 2024 at 07:52)
• Try this with a sequence of commands (39 messages, latest: Feb 22 2024 at 21:28)
• Are commands automatically rolled back on error? (3 messages, latest: Feb 22 2024 at 15:48)
• Parsing a string (6 messages, latest: Feb 22 2024 at 11:27)
• Can linters see tactic proofs? (24 messages, latest: Feb 21 2024 at 20:27)
• Qq function application (4 messages, latest: Feb 21 2024 at 10:08)
• Lean.Meta.forallTelescope and Lean.Meta.forallMetaTelescope (3 messages, latest: Feb 21 2024 at 10:06)
• ✔ attr which adds aesop rules with programmatic priority (4 messages, latest: Feb 20 2024 at 18:12)
• Qq/positivity confusion (14 messages, latest: Feb 18 2024 at 14:46)
• initialize_simp_projections is sometimes a placebo (1 message, latest: Feb 15 2024 at 22:34)
• differentiation tactic (43 messages, latest: Feb 15 2024 at 20:15)
• Aesop RuleTac restricted to a particular pattern (10 messages, latest: Feb 15 2024 at 16:41)
• Putting information in a goal (7 messages, latest: Feb 15 2024 at 16:02)
• Calling aesop from a tactic to obtain an Expr (10 messages, latest: Feb 15 2024 at 13:35)
• bound mixes gcongr and positivity (92 messages, latest: Feb 14 2024 at 21:49)
• aesop's destructProducts can add deps on implicit variables (9 messages, latest: Feb 12 2024 at 15:18)
• Aesop SimpleRuleTac vs SingleRuleTac (4 messages, latest: Feb 12 2024 at 15:12)
• Excessive Time and Memory Consumption of ProcessCommads (7 messages, latest: Feb 09 2024 at 14:02)
• Fun "regression" in ring_nf (not an actual regression) (4 messages, latest: Feb 06 2024 at 18:08)
• Memory handling in WithRpcRef (3 messages, latest: Feb 04 2024 at 11:33)
• omega with bit shifts (12 messages, latest: Jan 28 2024 at 21:01)
• WFTactics (1 message, latest: Jan 22 2024 at 14:44)
• solve_by_elim question (4 messages, latest: Jan 19 2024 at 23:36)
• deriving iterator (7 messages, latest: Jan 19 2024 at 00:18)
• Delaborator request (5 messages, latest: Jan 08 2024 at 05:28)
• Rubik's cube as a goal (1 message, latest: Jan 06 2024 at 17:48)
• commands elaborating … commands (4 messages, latest: Jan 05 2024 at 08:33)
• A simple result that omega fails to prove (58 messages, latest: Jan 05 2024 at 07:37)
• Counterexample for omega (6 messages, latest: Jan 04 2024 at 02:45)
• Making norm_num work for UInt64 (9 messages, latest: Dec 30 2023 at 20:54)
• simp_all removing a hypothesis before it can be used (13 messages, latest: Dec 23 2023 at 19:47)
• Forward chaining with aesop (8 messages, latest: Dec 23 2023 at 18:22)
• norm_num lemma function equalities (1 message, latest: Dec 21 2023 at 09:09)
• Positivity extension for Finset.card (58 messages, latest: Dec 14 2023 at 15:22)
• Detecting if interactive (7 messages, latest: Dec 11 2023 at 17:34)
• Inaccessible optional stuff (25 messages, latest: Dec 06 2023 at 04:10)
• Polimorphic lam Expr (7 messages, latest: Dec 01 2023 at 21:16)
• ring and scalar multiplication (5 messages, latest: Nov 27 2023 at 09:31)
• Modifying the reassoc attribute for monadic computations (24 messages, latest: Nov 17 2023 at 05:55)
• Hide intermediate goals from user? (3 messages, latest: Nov 16 2023 at 17:30)
• Help with writing tactic (213 messages, latest: Nov 06 2023 at 09:16)
• Issue writing a tactic (8 messages, latest: Nov 04 2023 at 16:41)
• Unexpander trouble (15 messages, latest: Nov 01 2023 at 21:59)
• ✔ destructured subtype pattern-match syntax (16 messages, latest: Oct 30 2023 at 13:23)
• Unexpanders: Book examples fail (4 messages, latest: Oct 28 2023 at 01:27)
• Determining whether a definition is recursive (11 messages, latest: Oct 25 2023 at 13:15)
• What to specify for addSuggestion (22 messages, latest: Oct 19 2023 at 21:29)
• Implicit Arguments in Rewrites (3 messages, latest: Oct 09 2023 at 09:27)
• Confusion with Pos.asNat traversing application (1 message, latest: Oct 08 2023 at 21:35)
• Taming positivity (45 messages, latest: Sep 17 2023 at 10:09)
• ✔ get all keys of attributes (3 messages, latest: Jul 30 2023 at 13:40)
• ifdef or macro templates (3 messages, latest: Jul 25 2023 at 01:17)
• Pattern matching optional Syntax (5 messages, latest: Jul 13 2023 at 16:35)
• ✔ multiline and indentation based syntax (2 messages, latest: Jul 13 2023 at 02:03)
• Metavariables in types of local hypotheses (9 messages, latest: Jul 12 2023 at 14:06)
• location of current decl (3 messages, latest: Jun 27 2023 at 11:55)
• Meta4dummies (3 messages, latest: Jun 08 2023 at 16:37)
• Alternative "toMessageData" for a list (7 messages, latest: Jun 04 2023 at 22:34)
• extractGoal (16 messages, latest: Jun 03 2023 at 20:48)
• meta tactic mode in Lean4? (11 messages, latest: Jun 03 2023 at 20:40)
• Dependent Arrows vs Fun (from MetaProgramming Book) (32 messages, latest: May 23 2023 at 11:39)
• Check type of a name (2 messages, latest: May 14 2023 at 19:21)
• ✔ aliasing a list of tactics (4 messages, latest: Apr 04 2023 at 05:47)
• ✔ abstract_local (5 messages, latest: Mar 01 2023 at 15:35)
• Working with Qq (1 message, latest: Feb 23 2023 at 01:35)
• How can I find if a subexpression occurs in a lean theo… (6 messages, latest: Feb 17 2023 at 10:54)
• Communicate between successive tactics (7 messages, latest: Jan 27 2023 at 12:15)
• Generating globally unique identifiers (4 messages, latest: Dec 12 2022 at 23:19)
• lift tries to clear hypotheses (8 messages, latest: Dec 09 2022 at 00:16)
• compare API (5 messages, latest: Dec 05 2022 at 01:43)
• json strings with newlines (7 messages, latest: Dec 01 2022 at 05:49)
• automatic lemmas retrieval (15 messages, latest: Nov 18 2022 at 14:03)
• register private name (2 messages, latest: Nov 17 2022 at 21:38)
• positivity fails (2 messages, latest: Nov 17 2022 at 21:37)
• ✔ Pattern matching on ite (3 messages, latest: Oct 14 2022 at 19:12)
• namespace, alias and open_locale (4 messages, latest: Oct 14 2022 at 07:31)
• Help on metaprogramming (5 messages, latest: Oct 10 2022 at 02:10)
• push_neg user command (3 messages, latest: Oct 06 2022 at 17:11)
• Call tactic by name (17 messages, latest: Oct 05 2022 at 22:10)
• New tactic: positivity (136 messages, latest: Oct 05 2022 at 15:59)
• ✔ Making a tactic more efficient (11 messages, latest: Sep 28 2022 at 13:51)
• Making a tactic more efficient (13 messages, latest: Sep 28 2022 at 13:47)
• Variants on mono (5 messages, latest: Sep 25 2022 at 13:48)
• Recursing with several tactics (15 messages, latest: Sep 23 2022 at 19:25)
• ✔ Tactic failure in a class (1 message, latest: Sep 23 2022 at 16:59)
• Selectively weaken norm_num (4 messages, latest: Sep 21 2022 at 22:58)
• alternative normal form for push_neg (4 messages, latest: Sep 21 2022 at 21:34)
• Tactic failure in a class (16 messages, latest: Sep 20 2022 at 18:38)
• advice on a tactic for decomposing inequalities (3 messages, latest: Sep 18 2022 at 16:09)
• eval_expr and universes (6 messages, latest: Sep 15 2022 at 09:33)
• apply_instance fails to infer instance? (17 messages, latest: Sep 12 2022 at 13:33)
• is_Type (8 messages, latest: Aug 31 2022 at 08:50)
• Match function application (6 messages, latest: Aug 24 2022 at 13:51)
• Interval arithmetic – what approach? (21 messages, latest: Aug 24 2022 at 09:18)
• norm_num on ennreal (28 messages, latest: Aug 03 2022 at 00:16)
• A tactic for expanding matrices into coefficients (17 messages, latest: Jul 28 2022 at 15:44)
• letI/exactI within do notation (4 messages, latest: Jul 28 2022 at 13:47)
• ✔ unexpected (by me) eval_expr behaviour (3 messages, latest: Jul 19 2022 at 02:53)
• inversion (6 messages, latest: Jul 14 2022 at 17:15)
• ✔ Parsing strings with def or theorem keywords (2 messages, latest: Jul 14 2022 at 16:55)
• Parsing strings with def or theorem keywords (7 messages, latest: Jul 14 2022 at 15:36)
• List of projections of structure (6 messages, latest: Jul 12 2022 at 13:52)
• ✔ structure with no fields is not a structure (1 message, latest: Jul 12 2022 at 12:52)
• structure with no fields is not a structure (8 messages, latest: Jul 10 2022 at 10:03)
• current file name (10 messages, latest: Jul 06 2022 at 18:10)
• variant syntax for congr' (96 messages, latest: Jun 30 2022 at 16:47)
• Instance diamonds in has_to_pexpr (6 messages, latest: Jun 22 2022 at 19:11)
• Custom binder (3 messages, latest: Jun 21 2022 at 15:28)
• ✔ WHNF of partially applied constants (3 messages, latest: Jun 15 2022 at 07:08)
• WHNF of partially applied constants (6 messages, latest: Jun 14 2022 at 19:07)
• tactic vs option (7 messages, latest: Jun 14 2022 at 09:36)
• avoid const_name? (25 messages, latest: Jun 13 2022 at 18:17)
• Backtracking parsers (32 messages, latest: Jun 10 2022 at 13:21)
• filtering an expr list for matches (12 messages, latest: Jun 10 2022 at 07:33)
• if exists assumption else (19 messages, latest: Jun 08 2022 at 11:52)
• listing explicit argument types (7 messages, latest: Jun 07 2022 at 15:38)
• to_expr behaves differently with an expected type (61 messages, latest: May 16 2022 at 23:58)
• tactic.result (4 messages, latest: May 16 2022 at 11:57)
• unification assignment (8 messages, latest: May 13 2022 at 15:18)
• naming metavariables after the fact (11 messages, latest: May 12 2022 at 10:51)
• passing types (23 messages, latest: May 12 2022 at 03:16)
• unify (28 messages, latest: May 10 2022 at 18:45)
• recursive tactic (12 messages, latest: May 10 2022 at 15:04)
• left-over metavariables (14 messages, latest: May 09 2022 at 01:31)
• sorting exprs that "are" nats (23 messages, latest: May 07 2022 at 03:40)
• passing functions (35 messages, latest: Apr 28 2022 at 07:15)
• loc.wildcard (4 messages, latest: Apr 25 2022 at 18:30)
• catching errors? (55 messages, latest: Apr 25 2022 at 17:55)
• concatenating and the tactic monad (39 messages, latest: Apr 22 2022 at 12:06)
• pattern-matching on a pexpr (4 messages, latest: Apr 22 2022 at 11:15)
• using ← inside a list of pexpr (45 messages, latest: Apr 20 2022 at 13:22)
• ✔ note with involved proof term (2 messages, latest: Apr 16 2022 at 13:49)
• note with involved proof term (2 messages, latest: Apr 16 2022 at 12:59)
• iterate until no change (16 messages, latest: Apr 15 2022 at 12:15)
• Building derive_handlers (4 messages, latest: Mar 28 2022 at 13:14)
• with_trace_errors (2 messages, latest: Mar 28 2022 at 12:36)
• parsing with ad hoc namespace (2 messages, latest: Mar 25 2022 at 16:51)
• interactive tactic printer (1 message, latest: Mar 25 2022 at 13:58)
• set tactic (55 messages, latest: Mar 23 2022 at 21:39)
• ✔ parsing specific ident (1 message, latest: Mar 15 2022 at 14:05)
• parsing specific ident (26 messages, latest: Mar 14 2022 at 20:53)
• ✔ parsing and collecting arguments as string (1 message, latest: Mar 14 2022 at 10:36)
• parsing and collecting arguments as string (1 message, latest: Mar 10 2022 at 16:45)
• faster interval_cases (6 messages, latest: Feb 28 2022 at 17:53)
• repeated exists_congr (15 messages, latest: Feb 20 2022 at 19:06)
• trivial case of linear_combination (15 messages, latest: Feb 15 2022 at 23:23)
• ✔ exact name (1 message, latest: Feb 08 2022 at 12:02)
• type instance failing with subtype (2 messages, latest: Feb 08 2022 at 10:28)
• exact name (7 messages, latest: Feb 07 2022 at 21:31)
• parsing type class instance (10 messages, latest: Feb 03 2022 at 10:34)
• all axioms used (20 messages, latest: Jan 31 2022 at 15:31)
• ✔ local_uniq_name providing strange names (3 messages, latest: Jan 30 2022 at 12:33)
• convert: why does it use reflexivity transparency.none? (4 messages, latest: Jan 29 2022 at 19:17)
• #2890 equiv_rw fails with metavariables (2 messages, latest: Jan 29 2022 at 17:38)
• unknown identifier error with user_notation (1 message, latest: Jan 29 2022 at 08:00)
• ✔ expression printer implemented in pure Lean (1 message, latest: Jan 28 2022 at 10:06)
• ✔ infer_type decl.value different from decl.type (4 messages, latest: Jan 28 2022 at 10:05)
• infer_type decl.value different from decl.type (9 messages, latest: Jan 28 2022 at 07:56)
• squeeze_simp - match failed?! (76 messages, latest: Jan 27 2022 at 19:26)
• expression printer implemented in pure Lean (9 messages, latest: Jan 26 2022 at 10:34)
• assumption with suggestions (31 messages, latest: Jan 25 2022 at 23:33)
• filter_upwards (17 messages, latest: Jan 25 2022 at 10:52)
• implicit of equality or iff (36 messages, latest: Jan 23 2022 at 16:39)
• See what a tactic does and roll back (8 messages, latest: Jan 19 2022 at 19:03)
• How does texpr parse numerals? (2 messages, latest: Jan 16 2022 at 07:27)
• Expressing parsing (34 messages, latest: Jan 15 2022 at 19:27)
• Code review for small tactic (28 messages, latest: Jan 11 2022 at 20:03)
• simulating interactive tactics in metaprogramming (18 messages, latest: Jan 11 2022 at 10:35)
• tactic parser (4 messages, latest: Jan 11 2022 at 02:31)
• interactive save_widget (42 messages, latest: Jan 07 2022 at 19:16)
• app builder unification problem (3 messages, latest: Dec 13 2021 at 15:37)
• observe (6 messages, latest: Nov 24 2021 at 14:02)
• get attributes on decl (5 messages, latest: Nov 11 2021 at 10:40)
• Teaching norm_num about complex numbers (20 messages, latest: Nov 09 2021 at 05:14)
• decl_noncomputable_reason (4 messages, latest: Oct 30 2021 at 10:48)
• Using the vm monad (7 messages, latest: Oct 25 2021 at 12:50)
• linarith tactic code (14 messages, latest: Oct 18 2021 at 15:48)
• using another tactic inside a meta function (8 messages, latest: Oct 17 2021 at 17:28)
• rcases quotient (14 messages, latest: Sep 17 2021 at 03:49)
• Testing has_repr (5 messages, latest: Aug 14 2021 at 14:48)
• Debugging tactic errors (8 messages, latest: Jul 06 2021 at 14:44)
• auto specialize (30 messages, latest: Jul 02 2021 at 11:02)
• linarith preprocessing (7 messages, latest: Jul 02 2021 at 06:31)
• Tactics outputting to STDOUT (4 messages, latest: Jun 16 2021 at 15:22)
• delayed_abstraction meta-variables (10 messages, latest: Jun 15 2021 at 22:29)
• Check for sorry in tactic proof (40 messages, latest: Jun 08 2021 at 20:58)
• writing large files (11 messages, latest: May 31 2021 at 19:56)
• io.iterate/forever and the state_t monad (7 messages, latest: May 31 2021 at 14:54)
• parser should fail (11 messages, latest: May 18 2021 at 16:41)
• Inaccessible names in tactic state (5 messages, latest: May 18 2021 at 15:26)
• nontriviality (17 messages, latest: May 18 2021 at 12:16)
• Capturing metavariable assignment (3 messages, latest: May 11 2021 at 13:01)
• cases' confuses the equation compiler (2 messages, latest: May 11 2021 at 13:00)
• User attribute caching (8 messages, latest: May 07 2021 at 17:21)
• how am I getting infinite recursion? (12 messages, latest: Apr 30 2021 at 15:52)
• error tolerant string parsing (13 messages, latest: Apr 22 2021 at 08:25)
• string replace (9 messages, latest: Apr 22 2021 at 00:51)
• help with rewriting simple tactic (1 message, latest: Apr 21 2021 at 19:54)
• match expression with unification (7 messages, latest: Apr 19 2021 at 09:42)
• finding terms of a certain type in a expr (13 messages, latest: Mar 03 2021 at 18:57)
• expr.mfold with branch pruning (19 messages, latest: Mar 02 2021 at 22:39)
• Introspecting a definition in a tactic (25 messages, latest: Feb 18 2021 at 09:59)
• Allowing focussing on multiple goals in case (15 messages, latest: Jan 27 2021 at 09:54)
• printing expr (4 messages, latest: Jan 24 2021 at 22:17)
• parse string literal (3 messages, latest: Jan 24 2021 at 14:02)
• Flat rintro (51 messages, latest: Jan 22 2021 at 18:41)
• parser documentation (5 messages, latest: Jan 22 2021 at 15:14)
• to_expr with hint (34 messages, latest: Jan 19 2021 at 19:51)
• change all goals (11 messages, latest: Jan 19 2021 at 15:29)
• simp with custom congruence lemmas (3 messages, latest: Jan 15 2021 at 10:42)
• Fetching all types with instances (37 messages, latest: Jan 14 2021 at 19:33)
• Should I use note invisibly (7 messages, latest: Jan 13 2021 at 15:15)
• generating a has_coe_to_fun in a tactic (7 messages, latest: Jan 08 2021 at 00:33)
• expr structure for coe_fun (16 messages, latest: Jan 08 2021 at 00:33)
• (no topic) (1 message, latest: Jan 07 2021 at 01:37)
• rw / clear - ident? (10 messages, latest: Jan 06 2021 at 11:21)
• tactic.induction does not keep case names (8 messages, latest: Jan 05 2021 at 19:35)
• parsing a list of expressions (3 messages, latest: Jan 02 2021 at 18:04)
• mk_app fails to retrieve declaration (18 messages, latest: Dec 20 2020 at 22:20)
• Allowing multiple targets in case (1 message, latest: Dec 18 2020 at 11:01)
• all_some vs traverse id (12 messages, latest: Dec 15 2020 at 15:00)
• norm_cast for algebras (8 messages, latest: Nov 25 2020 at 15:28)
• Autogenerating differentiable.exp etc (6 messages, latest: Nov 06 2020 at 23:07)
• cancel_denoms exercise (54 messages, latest: Nov 06 2020 at 17:57)
• access named arguments of declaration (36 messages, latest: Oct 29 2020 at 10:00)
• apply name (3 messages, latest: Oct 28 2020 at 13:29)
• has_lt for small inductive types (37 messages, latest: Oct 28 2020 at 10:42)
• get all lemmas in namespace (6 messages, latest: Oct 28 2020 at 08:44)
• elaborate pexpr into expr (18 messages, latest: Oct 27 2020 at 16:34)
• instance search in tactic (7 messages, latest: Oct 27 2020 at 14:05)
• Linear algebra tactic (26 messages, latest: Oct 20 2020 at 16:25)
• congr' is slow (35 messages, latest: Oct 20 2020 at 01:08)
• matching binders (20 messages, latest: Oct 18 2020 at 17:31)
• mutual recursion (11 messages, latest: Oct 18 2020 at 17:25)
• [Automatic apply lemmas for equivalences (and other bundle…](topic/Automatic.20apply.20lemmas.20for.20equivalences.20(and.20other.20bundle.2E.2E.2E.html) (24 messages, latest: Oct 18 2020 at 07:57)
• instances for meta defs (80 messages, latest: Oct 13 2020 at 10:18)
• Dependencies and local defs (2 messages, latest: Oct 13 2020 at 09:59)
• lemma distribution (12 messages, latest: Oct 05 2020 at 08:17)
• missing functionality in abel (2 messages, latest: Sep 30 2020 at 04:41)
• norm_num for modules (4 messages, latest: Sep 29 2020 at 10:25)
• cancel_denoms for vector spaces? (6 messages, latest: Sep 29 2020 at 07:34)
• Replacing the result (22 messages, latest: Sep 28 2020 at 17:12)
• Trace to stdout (9 messages, latest: Sep 22 2020 at 19:50)
• tactic modes(?) (61 messages, latest: Sep 19 2020 at 00:06)
• reformulate (17 messages, latest: Sep 16 2020 at 17:06)
• No-confusion for generalised inductive types (11 messages, latest: Sep 13 2020 at 14:25)
• succ_less tactic (10 messages, latest: Sep 13 2020 at 12:35)
• Tactics and universes (22 messages, latest: Sep 11 2020 at 15:35)
• Possible cause: occurs check failed (7 messages, latest: Sep 10 2020 at 00:06)
• measurable (1 message, latest: Aug 25 2020 at 12:41)
• basic parser use (34 messages, latest: Aug 07 2020 at 11:30)
• Registering a new option (5 messages, latest: Jul 21 2020 at 01:27)
• ? exercises (161 messages, latest: Jul 20 2020 at 11:32)
• dec_trivial (3 messages, latest: Jul 20 2020 at 08:15)
• to_expr failure (4 messages, latest: Jul 18 2020 at 15:32)
• constant polynomial tactic (14 messages, latest: Jun 21 2020 at 01:30)
• Getting started (7 messages, latest: May 24 2020 at 14:30)
• Lean Best Practices (10 messages, latest: May 23 2020 at 07:20)
• ideas for exercises (1 message, latest: May 17 2020 at 16:30)
• stream events (31 messages, latest: May 17 2020 at 14:19)

---

Last updated: May 02 2025 at 03:31 UTC