Zulip Chat Archive

Stream: metaprogramming / tactics

Topics:

"unknown free variable" in fun_prop (3 messages, latest: Feb 26 2026 at 12:59)
Use Tactic inside simproc (3 messages, latest: Feb 22 2026 at 09:13)
conflicting with Lean keywords (5 messages, latest: Feb 20 2026 at 21:27)
Odd behavior when using scoped syntax and withNamespace (3 messages, latest: Feb 20 2026 at 20:08)
Perfect sharing (6 messages, latest: Feb 20 2026 at 16:10)
Catch all exceptions (2 messages, latest: Feb 20 2026 at 09:00)
Calling Grind from MetaM (4 messages, latest: Feb 18 2026 at 21:03)
Deriving instance on a parameter of the target type (5 messages, latest: Feb 18 2026 at 15:35)
Type annotation for let in a monad (3 messages, latest: Feb 15 2026 at 19:58)
elaboration of nested actions: f (← t) (← u) (7 messages, latest: Feb 15 2026 at 18:16)
Check if a theorem is generated as a part of another one (3 messages, latest: Feb 12 2026 at 07:36)
Meta.check fails after revert (12 messages, latest: Feb 12 2026 at 07:33)
Eq.refl in cases and induction (5 messages, latest: Feb 12 2026 at 07:31)
Making a KeyedDeclsAttribute (23 messages, latest: Jan 28 2026 at 22:36)
InfoTree with ContextInfo from liftTermElabM (20 messages, latest: Jan 25 2026 at 18:49)
Why does the elaborator fail with conflicting syntax? (9 messages, latest: Jan 24 2026 at 06:16)
automatically declare helper classes (4 messages, latest: Jan 24 2026 at 02:56)
How can I prevent syntax from unfolding? (4 messages, latest: Jan 23 2026 at 15:01)
Include leading whitespace (9 messages, latest: Jan 20 2026 at 13:59)
Nested Delayed Assigned Metavariable (11 messages, latest: Jan 19 2026 at 08:02)
How do I match on syntax. (21 messages, latest: Jan 18 2026 at 19:17)
Parser matching ' or , (8 messages, latest: Jan 17 2026 at 02:15)
Force GC to run (36 messages, latest: Jan 13 2026 at 20:55)
Pretty printer parentheses (19 messages, latest: Jan 13 2026 at 20:32)
Current namespace in declaration elaborator (8 messages, latest: Jan 12 2026 at 09:57)
Unifying MVars with newly created FVars (10 messages, latest: Jan 12 2026 at 08:37)
Calling the parser at a point (17 messages, latest: Jan 10 2026 at 20:45)
simproc patterns tries to synth instances (4 messages, latest: Jan 09 2026 at 21:41)
Basic linter template (2 messages, latest: Jan 09 2026 at 19:35)
Access lake workspace during elaboration (5 messages, latest: Jan 08 2026 at 11:43)
Unfold let (5 messages, latest: Jan 07 2026 at 14:44)
Different behaviour in example and TermElabM (6 messages, latest: Jan 07 2026 at 10:18)
Add context for throwError (2 messages, latest: Jan 07 2026 at 08:06)
Grind Tactic : split/cases for non-inductive type (13 messages, latest: Jan 01 2026 at 21:53)
How to have an Expr? (5 messages, latest: Dec 31 2025 at 14:43)
Handling "partial matches" when unifying two terms (7 messages, latest: Dec 30 2025 at 15:12)
Check if a Lean.Name is roundtrippable (38 messages, latest: Dec 30 2025 at 04:44)
Inspecting function induction recursors in Lean 4 (4 messages, latest: Dec 29 2025 at 02:09)
Unexpect grind failure (7 messages, latest: Dec 26 2025 at 23:33)
Is there a substitute for polyrith yet? (6 messages, latest: Dec 20 2025 at 12:04)
Creating and registering structures without elabCommand (3 messages, latest: Dec 19 2025 at 09:16)
Theorem-level dependency graph (23 messages, latest: Dec 16 2025 at 20:31)
Recursor and RecursorInfo (6 messages, latest: Dec 15 2025 at 21:13)
Collect used external fvars in tactics block (3 messages, latest: Dec 14 2025 at 14:21)
Match on Expr in delaborator (4 messages, latest: Dec 11 2025 at 09:55)
Incremental elaboration of commands/caching (11 messages, latest: Dec 10 2025 at 12:57)
Infer/synthesize level metavariables (2 messages, latest: Dec 09 2025 at 18:27)
Delayed MVar Invocation (4 messages, latest: Dec 08 2025 at 18:50)
to_additive and module system (7 messages, latest: Dec 03 2025 at 22:48)
to_dual and structure projections (8 messages, latest: Dec 03 2025 at 13:41)
Metaprogramming in Lean 4 example (4 messages, latest: Nov 30 2025 at 16:56)
Allowed Prop projections in kernel vs check (17 messages, latest: Nov 25 2025 at 01:32)
Delaborators for IsOpen\[t\] etc (94 messages, latest: Nov 23 2025 at 13:26)
custom syntax outer conflicts (8 messages, latest: Nov 22 2025 at 19:36)
Apply different tactics to different goals? (9 messages, latest: Nov 20 2025 at 21:34)
dependent rewrite tactic (28 messages, latest: Nov 20 2025 at 09:50)
rewrite a tactic to a command (2 messages, latest: Nov 18 2025 at 10:05)
Parenthesizing custom syntax (3 messages, latest: Nov 17 2025 at 17:22)
ring/ bound/ simp/ grind (2 messages, latest: Nov 17 2025 at 00:06)
Disable hygiene for specific variables (5 messages, latest: Nov 12 2025 at 18:30)
Parsing integer literals (9 messages, latest: Nov 10 2025 at 18:41)
mutual induction tactic (66 messages, latest: Oct 30 2025 at 17:37)
Using forall binders as function binders (2 messages, latest: Oct 28 2025 at 19:53)
assumeInstancesCommute / assertInstancesCommute (6 messages, latest: Oct 27 2025 at 15:10)
scoped notation in an attribute (4 messages, latest: Oct 27 2025 at 12:29)
Renaming existing fields in structure? (7 messages, latest: Oct 27 2025 at 11:35)
How intro works with mvars (29 messages, latest: Oct 26 2025 at 21:40)
Parsing floats for a DSL (3 messages, latest: Oct 23 2025 at 14:24)
evaluating induction tactic within a tactic (6 messages, latest: Oct 20 2025 at 06:54)
Where is lambdaTelescopeReducing located? (6 messages, latest: Oct 10 2025 at 20:29)
Constructing syntax for natural number literal (8 messages, latest: Oct 10 2025 at 17:04)
isBoundedDefault not triggering (9 messages, latest: Oct 06 2025 at 10:00)
liftCommandElabM breaking namespace resolution? (3 messages, latest: Oct 05 2025 at 17:03)
How to distinguish constructors from functions (4 messages, latest: Oct 03 2025 at 15:44)
transport tactic (22 messages, latest: Oct 03 2025 at 00:28)
Debugging metaprogramming in TermElabM (3 messages, latest: Oct 01 2025 at 13:41)
Conditionally pretty-printing with spaces (5 messages, latest: Sep 30 2025 at 07:48)
Why getOptional? is not working for (tacticSeq)?? (4 messages, latest: Sep 30 2025 at 00:03)
abstractMVars not instantiating level mvars (7 messages, latest: Sep 29 2025 at 14:02)
pattern match against TSyntax and Bool (2 messages, latest: Sep 27 2025 at 19:32)
How to make a term of OfNat.ofNat i : Fin (n + 1) legally? (5 messages, latest: Sep 26 2025 at 15:01)
Elaborating a DSL that uses Lean's binders / PHOAS (3 messages, latest: Sep 26 2025 at 11:10)
Calling an Expr that has type MetaM in a MetaM program (10 messages, latest: Sep 25 2025 at 13:53)
Command to print the Expr of a Lean term? (19 messages, latest: Sep 13 2025 at 01:51)
Manipulating expressions with loose bvars (7 messages, latest: Sep 09 2025 at 14:09)
Destruct Tactic (1 message, latest: Sep 06 2025 at 21:12)
Helper functions for match? (3 messages, latest: Sep 06 2025 at 15:04)
Hygiene and shadowing (9 messages, latest: Sep 03 2025 at 17:39)
A Qq gotcha (12 messages, latest: Sep 01 2025 at 22:21)
Generated definition can #reduce but not #eval (11 messages, latest: Aug 31 2025 at 17:43)
Collect commands dependencies (3 messages, latest: Aug 26 2025 at 15:02)
Collect all dependencies required for an expression (17 messages, latest: Aug 25 2025 at 16:18)
declare_config_elab in term elaborator (5 messages, latest: Aug 22 2025 at 17:23)
Monomorphize Tactic (5 messages, latest: Aug 16 2025 at 20:37)
LeanGrow project (3 messages, latest: Aug 15 2025 at 22:35)
syntax with optional suffix (8 messages, latest: Aug 14 2025 at 12:26)
Solve level mvars in an expression (6 messages, latest: Aug 14 2025 at 00:07)
syntax with linebreaks (2 messages, latest: Aug 10 2025 at 12:09)
Macros that introduce non-level parameters (12 messages, latest: Aug 07 2025 at 22:21)
Imperative catches (12 messages, latest: Aug 07 2025 at 19:21)
Eq.ndrec (7 messages, latest: Aug 06 2025 at 23:19)
Instantiating type parameters of a polymorphic inductive typ (46 messages, latest: Aug 06 2025 at 23:12)
Introduction to tactic programming (114 messages, latest: Aug 06 2025 at 18:03)
precompileModules set causes initializer not found (2 messages, latest: Aug 06 2025 at 03:10)
MVarId.assign vs MVarId.checkedAssign vs isDefEq (10 messages, latest: Aug 05 2025 at 21:43)
writing a command to define (a family of) unexpanders (17 messages, latest: Aug 02 2025 at 05:53)
Direct changeLocalDecl' (5 messages, latest: Jul 31 2025 at 19:36)
Getting all simprocs (3 messages, latest: Jul 31 2025 at 09:53)
Parsing one tactic (10 messages, latest: Jul 31 2025 at 01:27)
isDefEq proofIrrelevance (6 messages, latest: Jul 29 2025 at 16:10)
syntax quotation and matching (15 messages, latest: Jul 29 2025 at 16:03)
Reducing match expressions in expression (5 messages, latest: Jul 27 2025 at 19:45)
Skip command if it doesn't parse (10 messages, latest: Jul 26 2025 at 15:23)
Separators for variadic syntax patterns (5 messages, latest: Jul 25 2025 at 00:09)
Extra spaces in prettyprinted term (7 messages, latest: Jul 23 2025 at 21:35)
Constructing docComment (3 messages, latest: Jul 23 2025 at 21:18)
add/remove (default := true) for aesop rule sets (4 messages, latest: Jul 23 2025 at 11:30)
Constructing a dependent product (3 messages, latest: Jul 22 2025 at 03:39)
Custom Deriving for Serialization Library (1 message, latest: Jul 21 2025 at 12:36)
Persisting hypotheses across tactics (28 messages, latest: Jul 18 2025 at 08:52)
Working with variables in a command (7 messages, latest: Jul 17 2025 at 17:31)
Generalized reduceProjs (2 messages, latest: Jul 17 2025 at 15:31)
Apply on hypothesis (16 messages, latest: Jul 17 2025 at 13:09)
defining notations with an attribute (6 messages, latest: Jul 15 2025 at 19:35)
Error Propagation with tryCatch (18 messages, latest: Jul 15 2025 at 16:02)
Matching generic Goals with Qq (25 messages, latest: Jul 15 2025 at 10:58)
constructor tactic (7 messages, latest: Jul 15 2025 at 10:09)
Move objects out of compacted region (1 message, latest: Jul 14 2025 at 02:29)
Question about unused variable linter (2 messages, latest: Jul 14 2025 at 00:06)
down to the axioms (100 messages, latest: Jul 13 2025 at 16:55)
Folding Syntax (4 messages, latest: Jul 11 2025 at 14:02)
Redundant brackets in syntax function application (8 messages, latest: Jul 11 2025 at 10:23)
✔ root prefix on TryThis TermSuggestion (7 messages, latest: Jul 11 2025 at 09:22)
✔ See raw value of a Expr variable (14 messages, latest: Jul 10 2025 at 18:47)
accessing theorems tagged by [match_pattern] (5 messages, latest: Jul 09 2025 at 14:25)
custom syntax (4 messages, latest: Jul 07 2025 at 21:15)
✔ trace for contradiction (8 messages, latest: Jul 05 2025 at 17:00)
Disable scoped notations during pretty printing (1 message, latest: Jul 04 2025 at 05:17)
Learning metaprogramming (18 messages, latest: Jul 03 2025 at 21:17)
Split theorem conclusion (9 messages, latest: Jul 03 2025 at 15:29)
✔ Passing Arguments to Deriving Handlers No Longer Suppor… (6 messages, latest: Jul 02 2025 at 13:55)
Qq context in run_tac (44 messages, latest: Jun 30 2025 at 08:59)
locating tactics and corresponding elaboration (14 messages, latest: Jun 28 2025 at 19:46)
Best way to monkeypatch existing tactics? (2 messages, latest: Jun 27 2025 at 19:27)
Idiomatic way to add declarations to a LocalContext (11 messages, latest: Jun 27 2025 at 19:18)
✔ Calculating the delta between two Environments (14 messages, latest: Jun 25 2025 at 22:00)
panic in Lean.Meta.getEqnsFor (4 messages, latest: Jun 23 2025 at 06:05)
✔ Prevent whnf from evaluating Nat.ble (5 messages, latest: Jun 22 2025 at 20:13)
Parsing a chain of characters (6 messages, latest: Jun 22 2025 at 16:41)
Proving the jealous mathematician riddle (1 message, latest: Jun 19 2025 at 18:02)
Best Practices for Renaming Variables in Exprs (5 messages, latest: Jun 18 2025 at 18:52)
✔ Detect whether a lemma is generated by simp (10 messages, latest: Jun 17 2025 at 17:47)
run meta program from command line (6 messages, latest: Jun 17 2025 at 14:49)
Changes in the parser (7 messages, latest: Jun 17 2025 at 09:20)
rw for inequalities (7 messages, latest: Jun 13 2025 at 15:45)
✔ Pretty printing term+tactic proofs (26 messages, latest: Jun 13 2025 at 07:10)
Parenthesizer error when creating do-blocks using TSyntax (3 messages, latest: Jun 13 2025 at 01:52)
✔ Challenging widget design (26 messages, latest: Jun 10 2025 at 03:51)
tactics for unfolding parameters defined in structure (5 messages, latest: Jun 09 2025 at 23:46)
Passing integer arguments in a tactic (9 messages, latest: Jun 08 2025 at 14:06)
Auxiliary information for delaboration (5 messages, latest: Jun 05 2025 at 21:02)
Goal changing when hypothesis is introduced (4 messages, latest: Jun 05 2025 at 11:09)
✔ Top-level delaborator (4 messages, latest: Jun 01 2025 at 15:42)
Deriving Instance for Inductives that have arguments (10 messages, latest: May 31 2025 at 15:02)
✔ Elaboration of syntax in lctx creates sorry (13 messages, latest: May 29 2025 at 01:06)
pattern-matching match (5 messages, latest: May 28 2025 at 15:18)
Reduce during typeclass search (11 messages, latest: May 28 2025 at 12:29)
withImportModules + #check/#print (2 messages, latest: May 25 2025 at 05:59)
Fancy syntax for syntax (3 messages, latest: May 22 2025 at 16:33)
Easiest way to get Repr from Unexpanders (10 messages, latest: May 22 2025 at 15:08)
✔ How to programatically declare inductives (10 messages, latest: May 22 2025 at 10:23)
Applying commutativity in "normal form" order (8 messages, latest: May 16 2025 at 16:38)
Adding to do-blocks in macros (1 message, latest: May 07 2025 at 04:40)
✔ 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)
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)
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)
✔ 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)
✔ 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)
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: Feb 28 2026 at 14:05 UTC