Zulip Chat Archive
Stream: lean4
Topics:
- New release of Functional Programming in Lean (145 messages, latest: Jan 31 2023 at 20:49)
- showing big_step is deterministic (9 messages, latest: Jan 31 2023 at 18:34)
- attributes on inductive constructors (1 message, latest: Jan 31 2023 at 17:42)
- How to prove properties about monad operations? (52 messages, latest: Jan 31 2023 at 16:57)
- ✔ Well-founded recursion on trees (26 messages, latest: Jan 31 2023 at 16:10)
- ownership / borrow-checking (2 messages, latest: Jan 31 2023 at 09:17)
- ✔ Task.spawn vs Promise.new (7 messages, latest: Jan 30 2023 at 20:07)
- nightly does not have binary lake (14 messages, latest: Jan 30 2023 at 18:51)
- variable (6 messages, latest: Jan 30 2023 at 15:37)
- valid occurrence of the datatypes … (6 messages, latest: Jan 30 2023 at 12:43)
- defining "type membership relation" (10 messages, latest: Jan 30 2023 at 10:08)
- Simp and funext (12 messages, latest: Jan 30 2023 at 07:25)
- Preserving a property through inductive constructions (1 message, latest: Jan 29 2023 at 22:01)
- #check issue with native_decide (7 messages, latest: Jan 29 2023 at 14:29)
- ✔ Meaning of
DefinitionSafety.partial
(10 messages, latest: Jan 28 2023 at 23:00) - naming hypotheses when using do-notation (5 messages, latest: Jan 28 2023 at 21:39)
- ✔ Problems simplifying conditions with hypotheses (37 messages, latest: Jan 28 2023 at 19:50)
- error loading library Aesop-Nanos.dll (23 messages, latest: Jan 28 2023 at 16:20)
- get filename + pos (5 messages, latest: Jan 28 2023 at 11:32)
- ✔ change with synthetic metavariables? (11 messages, latest: Jan 28 2023 at 08:42)
- hoisting a proof of termination to a separate definition (39 messages, latest: Jan 27 2023 at 19:20)
- JSX (11 messages, latest: Jan 27 2023 at 18:04)
- [tryResolve] fails on defeq instances (2 messages, latest: Jan 27 2023 at 15:57)
- emacs (57 messages, latest: Jan 27 2023 at 08:33)
- Something with universe levels (3 messages, latest: Jan 26 2023 at 06:40)
- Help with proof about lists (5 messages, latest: Jan 26 2023 at 05:15)
- where is better to put the type dependency info? (6 messages, latest: Jan 25 2023 at 22:33)
- Really simple question about decide (4 messages, latest: Jan 25 2023 at 21:53)
- weaker rfl after rw (3 messages, latest: Jan 25 2023 at 20:52)
- Inductive type Pair (8 messages, latest: Jan 25 2023 at 20:33)
- ✔ ForIn vs ForM (6 messages, latest: Jan 25 2023 at 20:03)
- Running lean from command line (11 messages, latest: Jan 25 2023 at 17:03)
- ✔ lake new with mathlib (25 messages, latest: Jan 25 2023 at 16:11)
- syntax/macros with iterated definitions (11 messages, latest: Jan 25 2023 at 08:19)
- simp vs rw with match witness (5 messages, latest: Jan 24 2023 at 21:23)
- Translating programs with
pre
post
conditions to Lean 4. (22 messages, latest: Jan 24 2023 at 20:05) calc
indentation (110 messages, latest: Jan 24 2023 at 09:32)- Access to the proof goal (3 messages, latest: Jan 24 2023 at 08:03)
- type class inference goes haywire (11 messages, latest: Jan 23 2023 at 18:53)
- equality vs decide equality (56 messages, latest: Jan 23 2023 at 17:22)
- Nontransitivity of DefEq (3 messages, latest: Jan 23 2023 at 14:04)
- Has Set been ported to Lean 4 yet? (3 messages, latest: Jan 23 2023 at 02:14)
- How to prove equality of
structure
s? (7 messages, latest: Jan 22 2023 at 22:46) - parentheses weirdness (13 messages, latest: Jan 22 2023 at 21:17)
- lake "build cycle detected" (12 messages, latest: Jan 21 2023 at 23:43)
- [simp? []](topic/simp.3F.20.5B.5D.html) (13 messages, latest: Jan 21 2023 at 21:56)
- conv congr implication (5 messages, latest: Jan 21 2023 at 19:11)
- inference of conditional conformance with type classes (12 messages, latest: Jan 21 2023 at 18:27)
- Conditional dependencies in lakefile (6 messages, latest: Jan 21 2023 at 14:40)
- simp/dsimp infinite recursion (8 messages, latest: Jan 21 2023 at 14:38)
- ✔ Proof about match (4 messages, latest: Jan 21 2023 at 13:38)
- unbalanced RBMap and RBSet (4 messages, latest: Jan 21 2023 at 11:43)
- ✔ How to make this code compile? (8 messages, latest: Jan 21 2023 at 10:25)
- product of categories (14 messages, latest: Jan 21 2023 at 03:42)
- csimp on recursors (18 messages, latest: Jan 20 2023 at 22:40)
- can't read "popup boxes" sometimes (23 messages, latest: Jan 20 2023 at 21:59)
- Verifying SAT formula (18 messages, latest: Jan 20 2023 at 19:28)
- Isomorphic products (4 messages, latest: Jan 20 2023 at 04:20)
#check <ident>
(15 messages, latest: Jan 19 2023 at 21:20)- Visualization Lean in VS Code (9 messages, latest: Jan 19 2023 at 20:38)
- Customize compile time error messages (6 messages, latest: Jan 19 2023 at 19:58)
- Lean 4 web editor (59 messages, latest: Jan 19 2023 at 16:31)
- Warn when a variable uses sorry (5 messages, latest: Jan 19 2023 at 15:46)
- ✔ Cast lemma (7 messages, latest: Jan 19 2023 at 14:42)
- Function.comp pretty printing (23 messages, latest: Jan 18 2023 at 22:18)
- Parsing idents separated by coma (11 messages, latest: Jan 18 2023 at 14:59)
- [RFC] Make autoImplicit default to false on non-greek (70 messages, latest: Jan 18 2023 at 14:46)
- Display of quantified statements (19 messages, latest: Jan 18 2023 at 14:12)
- #print prefix (14 messages, latest: Jan 18 2023 at 11:17)
- "Perfect world" dependency management (106 messages, latest: Jan 18 2023 at 11:07)
- Takeaways from proving Advent of Code solutions (12 messages, latest: Jan 18 2023 at 09:12)
- Message end position (4 messages, latest: Jan 17 2023 at 23:59)
- stricter #eval syntax (3 messages, latest: Jan 17 2023 at 23:43)
- \cdot in emacs (5 messages, latest: Jan 17 2023 at 23:17)
- Using lean 4 with python (2 messages, latest: Jan 17 2023 at 23:14)
- Branching on matched success/failure in monads (3 messages, latest: Jan 17 2023 at 22:48)
- dotted identifier notation error (1 message, latest: Jan 17 2023 at 21:05)
- elaborating from InfoTree (20 messages, latest: Jan 17 2023 at 18:11)
- Lake absolute rootdir (22 messages, latest: Jan 17 2023 at 17:26)
- elaboration in calc (6 messages, latest: Jan 17 2023 at 17:07)
- runFrontend on a lakefile.lean (6 messages, latest: Jan 17 2023 at 16:16)
- Core Stream class (57 messages, latest: Jan 17 2023 at 14:01)
- ✔ Using
aesop
to perform cases on a non-inductive type (1 message, latest: Jan 17 2023 at 11:06) - #eval, #check and line breaks in their messages (2 messages, latest: Jan 17 2023 at 10:20)
- Monadic op class design (3 messages, latest: Jan 17 2023 at 08:31)
- Extracting a proof from a dependent function call (11 messages, latest: Jan 17 2023 at 04:42)
- Why isn't Thunk a Monad? (6 messages, latest: Jan 16 2023 at 18:32)
- library_search not finding obvious proof (5 messages, latest: Jan 16 2023 at 16:51)
- hygiene question? (11 messages, latest: Jan 16 2023 at 10:04)
- Metaprogramming tutorial (252 messages, latest: Jan 15 2023 at 22:17)
- match_pattern attribute on Mul.mul (1 message, latest: Jan 15 2023 at 16:16)
- ∈ List.nil (12 messages, latest: Jan 15 2023 at 15:28)
- Changing a single field of a structure object (4 messages, latest: Jan 15 2023 at 15:03)
- instBEqNat = instBEq := rfl –fails (15 messages, latest: Jan 15 2023 at 07:08)
- ⊗ notation for types and elements (36 messages, latest: Jan 14 2023 at 19:50)
- Lake (8 messages, latest: Jan 14 2023 at 18:53)
- Lean4 AST (10 messages, latest: Jan 14 2023 at 18:51)
- Using
aesop
to perform cases on a non-inductive type (3 messages, latest: Jan 14 2023 at 16:53) - nested inductive datatypes parameters cannot contain local v (12 messages, latest: Jan 14 2023 at 12:40)
- If and match in conv mode (3 messages, latest: Jan 13 2023 at 22:37)
- parsing strings (62 messages, latest: Jan 13 2023 at 22:08)
- lake error (2 messages, latest: Jan 13 2023 at 20:30)
- List.range' not recognized (39 messages, latest: Jan 13 2023 at 16:18)
- Difference between extern and extern c? (9 messages, latest: Jan 13 2023 at 15:58)
- run_cmd and unsafe (15 messages, latest: Jan 13 2023 at 13:36)
- Proof automation (28 messages, latest: Jan 13 2023 at 06:49)
- web editor (27 messages, latest: Jan 12 2023 at 21:43)
- help reducing duplicated code (4 messages, latest: Jan 12 2023 at 14:12)
- algebraic effects and handlers? (15 messages, latest: Jan 12 2023 at 12:22)
- Spurious noncomputable tag (3 messages, latest: Jan 12 2023 at 01:39)
- Help representing a system (4 messages, latest: Jan 11 2023 at 22:03)
- Tactic to "apply" + "congr" (6 messages, latest: Jan 11 2023 at 18:09)
- port of LoVe (9 messages, latest: Jan 11 2023 at 16:34)
- syntax highlighting and infoview not working (4 messages, latest: Jan 11 2023 at 15:21)
- Lean comment syntax (10 messages, latest: Jan 11 2023 at 14:29)
- failed to synthesize Trans instance (7 messages, latest: Jan 11 2023 at 13:16)
- do we have
fillImplicitArgumentsWithFreshMVars
? (3 messages, latest: Jan 11 2023 at 11:57) - ✔ FFI to Rust/C++ (4 messages, latest: Jan 11 2023 at 11:06)
- Theorem Proving in Lean 4 in VSCode (2 messages, latest: Jan 10 2023 at 22:31)
- Cannot show termination of non-recursive function (8 messages, latest: Jan 10 2023 at 22:21)
copy message to comment
issue (3 messages, latest: Jan 10 2023 at 21:44)- theorems about dropWhile (14 messages, latest: Jan 10 2023 at 18:26)
- Lean doesn't unfold HAnd.hAnd (28 messages, latest: Jan 10 2023 at 17:27)
- data from constructor (8 messages, latest: Jan 10 2023 at 16:29)
- function definitions with ↦ (2 messages, latest: Jan 10 2023 at 07:54)
rewrite
tactic reaches maximum heartbeat (1 message, latest: Jan 10 2023 at 04:20)- free memory in the ffi (6 messages, latest: Jan 10 2023 at 02:41)
- Feature request: docstrings for instance fields (6 messages, latest: Jan 10 2023 at 02:09)
- Unexpander for function composition (1 message, latest: Jan 09 2023 at 21:22)
- change from Lean3 in dealing with open namespaces (12 messages, latest: Jan 09 2023 at 21:16)
- import local file (4 messages, latest: Jan 09 2023 at 13:53)
- Unfold partial function (4 messages, latest: Jan 09 2023 at 12:58)
- Can't get lean to unify equality (5 messages, latest: Jan 09 2023 at 12:26)
- Strong induction for List (8 messages, latest: Jan 09 2023 at 05:13)
- Pattern matching with arrays (8 messages, latest: Jan 08 2023 at 23:43)
- The state of the code generator (11 messages, latest: Jan 08 2023 at 17:55)
- Can't create new project (13 messages, latest: Jan 08 2023 at 17:33)
- When to [always_inline]? (13 messages, latest: Jan 08 2023 at 10:25)
- json output from lake build (2 messages, latest: Jan 08 2023 at 08:32)
- possible minor error in the fp in lean book? (2 messages, latest: Jan 08 2023 at 07:20)
- Importing Log breaks termination proof (57 messages, latest: Jan 08 2023 at 05:57)
- Equivalent to
_match_1
in Lean 4 (5 messages, latest: Jan 07 2023 at 17:25) - Doom Emacs setup (31 messages, latest: Jan 06 2023 at 22:46)
- printing to stdout (5 messages, latest: Jan 06 2023 at 22:24)
- Lean 4 not recognizing undefined variable (7 messages, latest: Jan 06 2023 at 21:02)
- C FFI usage (366 messages, latest: Jan 06 2023 at 17:04)
- code generator does not support recursor yet (9 messages, latest: Jan 06 2023 at 11:37)
- invalid {…} notation (6 messages, latest: Jan 06 2023 at 05:07)
- multiple reverts delete hypotheses (7 messages, latest: Jan 06 2023 at 02:54)
- New member question about possible bugs (4 messages, latest: Jan 05 2023 at 21:46)
- type class inference failure in pi type (4 messages, latest: Jan 05 2023 at 21:12)
- Σ (4 messages, latest: Jan 05 2023 at 11:53)
- Type checker slows down (3 messages, latest: Jan 04 2023 at 20:53)
- Prototype: Jupyter for Lean4 (42 messages, latest: Jan 04 2023 at 20:08)
- Prove return value of functon (4 messages, latest: Jan 04 2023 at 17:54)
- Boolean equality vs Prop equality (6 messages, latest: Jan 04 2023 at 17:36)
- Quick compiling of a single file (5 messages, latest: Jan 04 2023 at 14:01)
- type class inference looping (23 messages, latest: Jan 04 2023 at 09:32)
- Universes (19 messages, latest: Jan 03 2023 at 19:24)
- json parser and serializer (26 messages, latest: Jan 03 2023 at 18:22)
- ✔ Lean 4 VS Code extension help requestered squigly on im… (2 messages, latest: Jan 03 2023 at 11:16)
- Lean 4 VS Code extension help requestered squigly on im… (7 messages, latest: Jan 03 2023 at 09:53)
- locating non-lean files from tactics (2 messages, latest: Jan 03 2023 at 03:53)
- by interactive! (38 messages, latest: Jan 02 2023 at 21:47)
- Alternative to
#check
that does not show signatures? (4 messages, latest: Jan 02 2023 at 20:35) - passing instances explicitly (5 messages, latest: Jan 02 2023 at 19:43)
- jump to definition jumps to unimported file (1 message, latest: Jan 02 2023 at 18:57)
- Code action for showing the term of a tactic proof (5 messages, latest: Jan 02 2023 at 17:29)
- Aesop dev updates (10 messages, latest: Jan 02 2023 at 16:02)
- Syntax for constructor with explicit parameter (3 messages, latest: Jan 02 2023 at 15:40)
- ✔ Proving binary search terminates (7 messages, latest: Jan 02 2023 at 13:45)
- Docs: Manual Menu (2 messages, latest: Jan 02 2023 at 13:32)
- ✔ "ink" instead of "link" (10 messages, latest: Jan 02 2023 at 13:23)
- ✔ How to preserve intermediate results (1 message, latest: Jan 02 2023 at 07:00)
- ✔ Some chapters in the manual have become empty (4 messages, latest: Jan 01 2023 at 20:14)
- OfNat Pos (n+1) (3 messages, latest: Jan 01 2023 at 16:39)
- FFI to Rust/C++ (21 messages, latest: Dec 31 2022 at 21:55)
- How to preserve intermediate results (3 messages, latest: Dec 31 2022 at 19:03)
- ✔ FFI call C from within Lean (2 messages, latest: Dec 31 2022 at 17:55)
- FFI call C from within Lean (6 messages, latest: Dec 31 2022 at 16:00)
- expected parser to return exactly one syntax object (2 messages, latest: Dec 31 2022 at 14:53)
- Some chapters in the manual have become empty (2 messages, latest: Dec 31 2022 at 11:59)
- Expected token (11 messages, latest: Dec 30 2022 at 23:01)
- Trouble with standard library and imports (6 messages, latest: Dec 30 2022 at 22:54)
- Tactics for Nat arithmetic (12 messages, latest: Dec 30 2022 at 22:52)
- ✔ How to better compose/pipeline monads (1 message, latest: Dec 30 2022 at 22:40)
- panic! (40 messages, latest: Dec 30 2022 at 21:15)
- How to better compose/pipeline monads (10 messages, latest: Dec 30 2022 at 20:50)
- inverse of simple function (4 messages, latest: Dec 30 2022 at 17:38)
- ld64.lld dynamic link errors on MacOS (11 messages, latest: Dec 30 2022 at 12:13)
- ✔ normal code => explicit Expr? (3 messages, latest: Dec 30 2022 at 10:08)
- normal code => explicit Expr? (6 messages, latest: Dec 30 2022 at 09:15)
- Is there a tutorial for lean's module and package system? (4 messages, latest: Dec 30 2022 at 02:03)
- initializing data from IO (15 messages, latest: Dec 30 2022 at 01:35)
- ✔ How to solve the problem of universe level too big? (4 messages, latest: Dec 29 2022 at 07:09)
- How to solve the problem of universe level too big? (1 message, latest: Dec 29 2022 at 06:52)
- C.2.2.1 vs. C.3 (2 messages, latest: Dec 29 2022 at 06:36)
- ✔
() and
: comparing Lean 3 and 4 (7 messages, latest: Dec 29 2022 at 05:34) - while let (6 messages, latest: Dec 28 2022 at 22:00)
- Sigma.mk and length-n-tuples (3 messages, latest: Dec 28 2022 at 15:34)
() and
: comparing Lean 3 and 4 (2 messages, latest: Dec 28 2022 at 10:34)- Widgets in vscode (20 messages, latest: Dec 27 2022 at 22:57)
- Syntax quotation (1 message, latest: Dec 27 2022 at 21:49)
- CPS and tail recursion (18 messages, latest: Dec 27 2022 at 19:11)
- "motive is not type correct" meaning (29 messages, latest: Dec 27 2022 at 18:39)
- unknown identifier (12 messages, latest: Dec 27 2022 at 17:39)
- ✔ Show constructors are injective and non-overlapping (1 message, latest: Dec 27 2022 at 14:46)
- Show constructors are injective and non-overlapping (4 messages, latest: Dec 27 2022 at 05:49)
- can't synthesize argument (5 messages, latest: Dec 26 2022 at 20:04)
- notation (6 messages, latest: Dec 26 2022 at 17:26)
- equality type and equality of types (7 messages, latest: Dec 25 2022 at 20:56)
- Elaborating unknown identifiers (1 message, latest: Dec 25 2022 at 15:31)
- Nix doesn't like filenames with '!' (3 messages, latest: Dec 25 2022 at 14:42)
- proof in monad contexts (15 messages, latest: Dec 25 2022 at 10:23)
- typeclass instance problem is stuck (7 messages, latest: Dec 24 2022 at 22:38)
- Teaching resources / Lean Game Maker for Lean 4 (1 message, latest: Dec 24 2022 at 12:47)
- Is there a way to use equality of pattern in the case? (3 messages, latest: Dec 24 2022 at 06:53)
- lean 3 or lean 4 (9 messages, latest: Dec 23 2022 at 21:27)
- Lean -o confusing error message (4 messages, latest: Dec 23 2022 at 20:35)
- [lake build
](topic/lake.20build.20.3Cpath.3E.html) (7 messages, latest: Dec 23 2022 at 20:11) - Optimize repo with Git-lfs (1 message, latest: Dec 23 2022 at 16:59)
- Tactics for splitting if statements (8 messages, latest: Dec 23 2022 at 04:15)
- Possible bug with lake update (2 messages, latest: Dec 23 2022 at 02:09)
- ✔ What role does a file play in namespace hierarchy? (9 messages, latest: Dec 22 2022 at 18:24)
- 7 ∧ / ∨ (34 messages, latest: Dec 22 2022 at 12:23)
- Nix builds (154 messages, latest: Dec 22 2022 at 11:17)
- OO polymorphism? (85 messages, latest: Dec 22 2022 at 08:15)
- Call Function in Shared Library (5 messages, latest: Dec 22 2022 at 05:50)
- Easily test lean4 patch (4 messages, latest: Dec 22 2022 at 01:48)
- ✔ Easily test lean4 patch (12 messages, latest: Dec 22 2022 at 00:40)
- Float design document (30 messages, latest: Dec 21 2022 at 23:17)
- Proof by cases of finite integer (23 messages, latest: Dec 21 2022 at 18:52)
- simp at h has no effect but changes subsequent tactics? (21 messages, latest: Dec 21 2022 at 17:46)
- conv tactic
arg
(11 messages, latest: Dec 21 2022 at 15:14) - Elaborator regression from Lean3 (1 message, latest: Dec 21 2022 at 10:35)
- Functional Programming in Lean (7 messages, latest: Dec 20 2022 at 22:05)
mk_simp_attr
(7 messages, latest: Dec 20 2022 at 22:02)- keywords changed from lean 3 (11 messages, latest: Dec 20 2022 at 20:02)
- ✔ Last two explicit arguments (2 messages, latest: Dec 20 2022 at 15:32)
- ✔ injectivity of inductive type function (15 messages, latest: Dec 20 2022 at 15:16)
- lake build Mathlib.Foo (1 message, latest: Dec 20 2022 at 14:42)
- injectivity of inductive type function (2 messages, latest: Dec 20 2022 at 14:02)
- Last two explicit arguments (1 message, latest: Dec 20 2022 at 10:58)
- Syntax for defining functions with implicit variables (2 messages, latest: Dec 20 2022 at 04:31)
- map out of restricted comprehension (5 messages, latest: Dec 20 2022 at 00:17)
- add_decl_doc panic loop (26 messages, latest: Dec 19 2022 at 22:24)
- help with
unfold
(18 messages, latest: Dec 19 2022 at 20:36) - Bvars (7 messages, latest: Dec 19 2022 at 15:22)
- profiling declarations (1 message, latest: Dec 19 2022 at 15:08)
- incorrect assumption about dot notation declaration name (3 messages, latest: Dec 19 2022 at 12:46)
- ✔ Why goal in context? (2 messages, latest: Dec 18 2022 at 15:47)
- Why goal in context? (3 messages, latest: Dec 18 2022 at 14:52)
- semantic highlighting in dependent match (1 message, latest: Dec 18 2022 at 11:19)
- [RFC] Revise
Std.Range
(6 messages, latest: Dec 18 2022 at 07:54) - unused variable bug? (16 messages, latest: Dec 17 2022 at 23:53)
- simp working only after dsimp (7 messages, latest: Dec 17 2022 at 19:37)
- bug in included variables (31 messages, latest: Dec 17 2022 at 17:19)
- tactic combinator <|> (5 messages, latest: Dec 17 2022 at 00:10)
- partial & while (3 messages, latest: Dec 16 2022 at 23:51)
- ✔ for/if let (2 messages, latest: Dec 16 2022 at 23:36)
- while foo := f () do (4 messages, latest: Dec 16 2022 at 22:54)
- possible linter bugs (18 messages, latest: Dec 16 2022 at 21:38)
- sup/Sup (52 messages, latest: Dec 16 2022 at 11:54)
- ✔ Shorthand for function composition? (1 message, latest: Dec 16 2022 at 10:42)
- ✔ continue proof after <;> (or workaround) (6 messages, latest: Dec 15 2022 at 21:40)
- more auxDecl problems (2 messages, latest: Dec 15 2022 at 21:01)
- Shorthand for function composition? (7 messages, latest: Dec 15 2022 at 17:22)
- server error (14 messages, latest: Dec 15 2022 at 16:02)
alias
unfolds definitions (1 message, latest: Dec 15 2022 at 12:45)- using (or making explicit) hidden assumptions? (4 messages, latest: Dec 15 2022 at 05:38)
- ✔ How do you refer to instances in Lean4? (9 messages, latest: Dec 15 2022 at 02:10)
- quote4 match error "resulting term contains metavariable" (4 messages, latest: Dec 15 2022 at 00:48)
- maps out of dependent product (3 messages, latest: Dec 14 2022 at 20:45)
- unique constituent of the unit (2 messages, latest: Dec 14 2022 at 19:25)
- quote4 match error (1 message, latest: Dec 14 2022 at 19:06)
- undefined in Lean4 (5 messages, latest: Dec 14 2022 at 13:16)
- ✔ Lean can convert between Bool and Prop? How? (4 messages, latest: Dec 14 2022 at 11:10)
- Lean can convert between Bool and Prop? How? (2 messages, latest: Dec 14 2022 at 11:02)
- <;> in
TacticM
? (4 messages, latest: Dec 14 2022 at 10:23) - tactic 'cases' failed nested error (13 messages, latest: Dec 13 2022 at 21:19)
- dunfold in lean4 (1 message, latest: Dec 13 2022 at 21:01)
- Using repeat as identifier (6 messages, latest: Dec 13 2022 at 19:49)
- simp only sigma (4 messages, latest: Dec 13 2022 at 17:41)
- definition of a limit (5 messages, latest: Dec 13 2022 at 15:26)
- ✔ finding number/list of arguments? (8 messages, latest: Dec 13 2022 at 11:19)
- finding number/list of arguments? (12 messages, latest: Dec 13 2022 at 10:40)
- confusing Qq error (12 messages, latest: Dec 13 2022 at 07:16)
- linker errors (4 messages, latest: Dec 13 2022 at 04:28)
- list comprehension (2 messages, latest: Dec 13 2022 at 03:53)
- Stack overflow in for loops? (10 messages, latest: Dec 12 2022 at 22:01)
- attributes attached to a declaration (10 messages, latest: Dec 12 2022 at 12:11)
- Parser.trailingLoop (3 messages, latest: Dec 12 2022 at 10:55)
- Integer division (5 messages, latest: Dec 11 2022 at 20:07)
- Definitional double negation in intuitionistic logic (4 messages, latest: Dec 11 2022 at 05:21)
- VS Code syntax highlighting (26 messages, latest: Dec 11 2022 at 02:38)
- ✔ Mutable nested structure (10 messages, latest: Dec 10 2022 at 15:07)
- compling one file in a project (3 messages, latest: Dec 10 2022 at 13:09)
- Proving properties of partial functions (33 messages, latest: Dec 09 2022 at 23:34)
- iterating over
Fin n
(10 messages, latest: Dec 09 2022 at 19:36) - How to prove ∀ {x : α}, p x without introducing x (7 messages, latest: Dec 09 2022 at 18:09)
(_)
vs_
syntax (45 messages, latest: Dec 09 2022 at 15:28)- ✔ Custom eliminators (1 message, latest: Dec 09 2022 at 12:44)
- Custom eliminators (6 messages, latest: Dec 09 2022 at 11:43)
- match pattern not rfl-ing with match argument (3 messages, latest: Dec 08 2022 at 22:21)
- match pattern not rfl-ing (7 messages, latest: Dec 08 2022 at 21:24)
- [RFC] refine_struct functionality via new ?.. syntax (211 messages, latest: Dec 08 2022 at 21:21)
- Unification issue involving OfNat (7 messages, latest: Dec 08 2022 at 16:37)
- VS Code (4 messages, latest: Dec 08 2022 at 16:04)
- precedence of
;
/<;>
vstry
/repeat
(32 messages, latest: Dec 08 2022 at 15:31) - What type annotation can do (3 messages, latest: Dec 08 2022 at 13:24)
- Learning about metaprogramming (12 messages, latest: Dec 08 2022 at 05:42)
- Compiler stuck computing something… (63 messages, latest: Dec 08 2022 at 02:05)
- unnecessarily tombstoned argument (3 messages, latest: Dec 08 2022 at 01:43)
- "unknown goal" bug (17 messages, latest: Dec 07 2022 at 14:20)
- guess the import (4 messages, latest: Dec 07 2022 at 12:41)
- Reading a File (47 messages, latest: Dec 07 2022 at 09:29)
- Array boundary check (9 messages, latest: Dec 07 2022 at 01:11)
- "this" with implicit arguments (8 messages, latest: Dec 06 2022 at 13:58)
- Lean 4 vs Idris 2 (52 messages, latest: Dec 06 2022 at 13:29)
- Refer to currently defined struct (3 messages, latest: Dec 06 2022 at 10:47)
- Showing hygienic binder names (3 messages, latest: Dec 06 2022 at 08:45)
- ✔ Lean doesn't try to coerce (2 messages, latest: Dec 06 2022 at 01:47)
- Lean doesn't try to coerce (9 messages, latest: Dec 05 2022 at 19:05)
- Fixed precision signed integer types (11 messages, latest: Dec 05 2022 at 16:53)
- ✔ Custom Lean Server cannot find native code (2 messages, latest: Dec 05 2022 at 15:23)
- Custom Lean Server cannot find native code (2 messages, latest: Dec 05 2022 at 14:55)
- FFI (2 messages, latest: Dec 05 2022 at 11:42)
- ✔ grug ponders the universe (7 messages, latest: Dec 05 2022 at 10:03)
- Formalizing Gardam's disproof of a "Kaplansky Conjecture" (25 messages, latest: Dec 05 2022 at 02:17)
- Computed fields with implicit parameters (1 message, latest: Dec 04 2022 at 23:16)
- Run the
CoreM
monad from frontend (1 message, latest: Dec 04 2022 at 17:44) - elaboration of coercions (5 messages, latest: Dec 04 2022 at 16:02)
- Custom hovers in VSCode (2 messages, latest: Dec 04 2022 at 08:41)
- unfold_projs (2 messages, latest: Dec 04 2022 at 01:38)
- Unwrap Except (3 messages, latest: Dec 03 2022 at 20:53)
- doc-gen4 (55 messages, latest: Dec 03 2022 at 16:54)
- Speed and time stamps in Lean 4 (6 messages, latest: Dec 03 2022 at 15:30)
- Implicit arguments in Equivalence (2 messages, latest: Dec 02 2022 at 22:26)
- Natural Number Game in WebAssembly (3 messages, latest: Dec 02 2022 at 15:54)
- by_cases renames wrong hypothesis (12 messages, latest: Dec 02 2022 at 15:38)
- ✔ pretty printing custom syntax (9 messages, latest: Dec 02 2022 at 13:57)
- Showing functions in an unsafe way (26 messages, latest: Dec 02 2022 at 10:28)
- elaborate rwRule (2 messages, latest: Dec 02 2022 at 09:08)
- return from repeat (5 messages, latest: Dec 02 2022 at 08:56)
mutual
by default (6 messages, latest: Dec 02 2022 at 08:52)- "binary package was not provided for 'linux'" on Ubuntu (23 messages, latest: Dec 02 2022 at 06:27)
- ✔ Infinite For Loop (2 messages, latest: Dec 02 2022 at 06:17)
- Bug in sizeOf generation (1 message, latest: Dec 02 2022 at 05:56)
- Infinite For Loop (3 messages, latest: Dec 02 2022 at 04:42)
- ✔ Random Number Generation (1 message, latest: Dec 02 2022 at 03:23)
- ✔ Terse code (3 messages, latest: Dec 02 2022 at 03:22)
- Terse code (8 messages, latest: Dec 02 2022 at 03:04)
- ✔ Parse Nat from String (2 messages, latest: Dec 02 2022 at 01:39)
- Parse Nat from String (2 messages, latest: Dec 02 2022 at 01:23)
- ✔ Lean 4 vs Idris 2 (2 messages, latest: Dec 02 2022 at 01:08)
- Random Number Generation (2 messages, latest: Dec 02 2022 at 01:08)
- Warning when I use a constant function (2 messages, latest: Dec 02 2022 at 00:19)
- getting from #eval to a proof. (9 messages, latest: Dec 01 2022 at 21:24)
- Procedural programming with arrays (7 messages, latest: Dec 01 2022 at 19:39)
- translating
prod.lex_wf
to Lean 4 (7 messages, latest: Dec 01 2022 at 17:01) - Termination in Computed Fields (1 message, latest: Dec 01 2022 at 15:02)
- Reader and local (7 messages, latest: Dec 01 2022 at 09:27)
- HashMap with inductive types? (4 messages, latest: Nov 30 2022 at 13:53)
- Did I write something wrong? (4 messages, latest: Nov 30 2022 at 13:50)
- getLCtx and have (3 messages, latest: Nov 30 2022 at 13:20)
- ✔ Making sense of universes (3 messages, latest: Nov 30 2022 at 12:32)
- structure not picking up unnecessary typeclass (2 messages, latest: Nov 30 2022 at 11:12)
- Structural induction for nested inductive types (7 messages, latest: Nov 30 2022 at 08:59)
- why doesn't this unify? (16 messages, latest: Nov 29 2022 at 22:37)
- make binder implicit in CoeFun (14 messages, latest: Nov 29 2022 at 22:35)
- LeanAide translation: Natural language to Lean 4 (1 message, latest: Nov 29 2022 at 03:40)
- Structural recursion for reflexive inductive type (1 message, latest: Nov 28 2022 at 21:52)
- reducing String.data (12 messages, latest: Nov 28 2022 at 18:06)
- Nontrivial HEq (4 messages, latest: Nov 28 2022 at 17:10)
- reformat script (12 messages, latest: Nov 28 2022 at 14:50)
- error while building Lean 4 (8 messages, latest: Nov 28 2022 at 14:34)
- equation compiler magic in lean4 (44 messages, latest: Nov 28 2022 at 07:46)
- How to search for counterexamples in the proof (3 messages, latest: Nov 27 2022 at 12:59)
- ✔ expected '{' or strict indendation (8 messages, latest: Nov 27 2022 at 09:52)
- expected '{' or strict indendation (1 message, latest: Nov 27 2022 at 04:03)
- importing file with
#exit
in (5 messages, latest: Nov 26 2022 at 22:55) - sometimes I can't read the hovers in VS Code (2 messages, latest: Nov 26 2022 at 22:29)
- json parse and serializer (1 message, latest: Nov 26 2022 at 20:39)
- Implicit arguments (1 message, latest: Nov 26 2022 at 14:43)
- Derived/declared instance naming (1 message, latest: Nov 26 2022 at 11:34)
- ✔ Semantic Highlighting of Literals (1 message, latest: Nov 25 2022 at 20:53)
- ✔ What do e@, nm@ stand for? (1 message, latest: Nov 25 2022 at 14:06)
- Does Lean Have a Symbol Primitive? (15 messages, latest: Nov 25 2022 at 13:47)
- What do e@, nm@ stand for? (2 messages, latest: Nov 25 2022 at 13:41)
- Heads up: Lake changes in latest nightly (4 messages, latest: Nov 25 2022 at 13:38)
- generalizing @[widget] (3 messages, latest: Nov 25 2022 at 04:21)
- Package decl with IO (4 messages, latest: Nov 24 2022 at 23:07)
- Semantic Highlighting of Literals (3 messages, latest: Nov 24 2022 at 21:24)
- applySimpResultToProp variant (1 message, latest: Nov 24 2022 at 11:49)
- genearlizing @[widget] (1 message, latest: Nov 24 2022 at 07:56)
- Error loading library 126 when building (4 messages, latest: Nov 24 2022 at 01:06)
- tactics should fail if they do nothing? (15 messages, latest: Nov 23 2022 at 22:14)
- Conditional Syntax (11 messages, latest: Nov 23 2022 at 20:10)
- Unfolding type class definitions in order to rewrite (8 messages, latest: Nov 23 2022 at 16:49)
- ✔ Golfable proof? (1 message, latest: Nov 23 2022 at 16:21)
- breadcrumb confusion (3 messages, latest: Nov 23 2022 at 14:52)
- Getting instance priority/AttributeKind (1 message, latest: Nov 23 2022 at 13:09)
- Surprising namespaces in elaboration of type of function (10 messages, latest: Nov 23 2022 at 10:13)
- copy code from alectryon (7 messages, latest: Nov 23 2022 at 09:07)
- Golfable proof? (4 messages, latest: Nov 23 2022 at 03:49)
- Generalize doing reductions? (1 message, latest: Nov 23 2022 at 00:28)
- Broken compilation (21 messages, latest: Nov 22 2022 at 01:14)
- recursive definition in structure fields (8 messages, latest: Nov 21 2022 at 18:37)
- Interactive Svg (17 messages, latest: Nov 21 2022 at 18:22)
- SimpTheorems.addDeclToUnfold vs mkSimpAttr (1 message, latest: Nov 21 2022 at 16:40)
- CoeHTCT synthesis timing out with default args and coercions (18 messages, latest: Nov 21 2022 at 09:59)
- Gory details of
coe
(6 messages, latest: Nov 21 2022 at 07:11) - Lean equivalent of MACROEXPAND-1? (6 messages, latest: Nov 20 2022 at 20:39)
- Typing issue in Lean 4 through Equiv (3 messages, latest: Nov 19 2022 at 21:55)
- phantom errors (3 messages, latest: Nov 19 2022 at 16:36)
- [✔ Lean 3 decl_meta_info turns into Lean 4 __?](topic/.E2.9C.94.20Lean.203.20decl_meta_info.20turns.20into.20Lean.204.20__.3F.html) (6 messages, latest: Nov 19 2022 at 01:30)
- [Lean 3 decl_meta_info turns into Lean 4 __?](topic/Lean.203.20decl_meta_info.20turns.20into.20Lean.204.20__.3F.html) (1 message, latest: Nov 19 2022 at 00:00)
- adding definitions (35 messages, latest: Nov 18 2022 at 20:47)
- Lean private objects (2 messages, latest: Nov 18 2022 at 19:52)
- Syntax pos to LSP pos (47 messages, latest: Nov 18 2022 at 18:25)
- code action behaviour? (29 messages, latest: Nov 18 2022 at 17:25)
- mathlib4 (3 messages, latest: Nov 18 2022 at 16:06)
- Beginner question on rfl (6 messages, latest: Nov 18 2022 at 15:40)
- indenting after "by" (24 messages, latest: Nov 18 2022 at 08:00)
- Failed to elaborate eliminator (14 messages, latest: Nov 18 2022 at 07:35)
- lean-toolchain (1 message, latest: Nov 17 2022 at 19:21)
- Interactive definitions using the InfoView (2 messages, latest: Nov 17 2022 at 16:29)
- ✔ thunk simp (7 messages, latest: Nov 17 2022 at 13:48)
- PANIC at Lean.Meta.whnfEasyCases (4 messages, latest: Nov 17 2022 at 01:30)
Std.DList
vsStd.Data.DList
(3 messages, latest: Nov 17 2022 at 01:01)- Errors from widgets (11 messages, latest: Nov 16 2022 at 22:44)
- Tactic tutorial (26 messages, latest: Nov 16 2022 at 21:57)
- Finding reduced typeclass instances (6 messages, latest: Nov 16 2022 at 17:35)
- What to do to report an error? (18 messages, latest: Nov 16 2022 at 16:25)
- dedup (2 messages, latest: Nov 16 2022 at 16:02)
- nix setup for lean4 (5 messages, latest: Nov 16 2022 at 15:08)
- Bug: No autocomplete on even chars (7 messages, latest: Nov 16 2022 at 14:00)
- Performance drop (55 messages, latest: Nov 16 2022 at 08:31)
- Precompile specific modules (46 messages, latest: Nov 16 2022 at 04:24)
- ✔ funext (8 messages, latest: Nov 15 2022 at 22:26)
- SatisfiesM.and (9 messages, latest: Nov 15 2022 at 17:34)
- lean4#1829 (2 messages, latest: Nov 15 2022 at 17:28)
- simp lemma with variable head (4 messages, latest: Nov 15 2022 at 17:20)
(kernel) declaration has metavariables
error (1 message, latest: Nov 15 2022 at 16:51)- Commutative Diagram Widget (3 messages, latest: Nov 15 2022 at 10:41)
- Disable certain notation (4 messages, latest: Nov 15 2022 at 07:36)
- mkNullNode (19 messages, latest: Nov 14 2022 at 16:09)
- lean-sys update (1 message, latest: Nov 14 2022 at 13:14)
- application type mismatch in example (4 messages, latest: Nov 14 2022 at 10:31)
- ✔
many
combinator and backtracking (3 messages, latest: Nov 13 2022 at 18:07) many
combinator and backtracking (3 messages, latest: Nov 13 2022 at 17:56)- New std4 linters (1 message, latest: Nov 13 2022 at 09:29)
- make syntax cat accept empty string (16 messages, latest: Nov 13 2022 at 08:30)
- Blanks in apply (2 messages, latest: Nov 12 2022 at 16:09)
- Nat.sqrt (31 messages, latest: Nov 12 2022 at 01:45)
- ✔ elab a term within a tactic (2 messages, latest: Nov 11 2022 at 21:06)
- elab a term within a tactic (7 messages, latest: Nov 11 2022 at 20:34)
- Can I try a tactic during elaboration? (22 messages, latest: Nov 11 2022 at 14:32)
- Heartbeats (10 messages, latest: Nov 11 2022 at 14:22)
- Opaque let binding in simp (3 messages, latest: Nov 11 2022 at 10:52)
- thunk simp (2 messages, latest: Nov 11 2022 at 08:31)
- Unification of LE of Int and Preorder (1 message, latest: Nov 11 2022 at 03:31)
- standalone deriving (3 messages, latest: Nov 11 2022 at 01:18)
- ✔ Parser bug? (1 message, latest: Nov 10 2022 at 22:34)
- ✔ Appending indices to Names (2 messages, latest: Nov 10 2022 at 21:26)
- existsi for already elaborated Expr (18 messages, latest: Nov 10 2022 at 20:38)
- Parser bug? (7 messages, latest: Nov 10 2022 at 20:11)
@\[class\] structure
!=class
? (7 messages, latest: Nov 10 2022 at 19:29)- How to get the imports for a given module? (3 messages, latest: Nov 10 2022 at 18:43)
- Syntax match not forcing types (4 messages, latest: Nov 10 2022 at 15:46)
- Appending indices to Names (3 messages, latest: Nov 10 2022 at 10:26)
- higher order unification failure (13 messages, latest: Nov 09 2022 at 22:28)
- When do "placeholder contexts" get synthesized? (4 messages, latest: Nov 09 2022 at 21:52)
- ✔ Environment extensions (4 messages, latest: Nov 09 2022 at 16:43)
- Environment extensions (4 messages, latest: Nov 09 2022 at 16:02)
- unifying ⦃x y⦄ with {x y} (5 messages, latest: Nov 09 2022 at 14:14)
- ✔ appendMCtx or mergeMCtx (4 messages, latest: Nov 08 2022 at 09:49)
- appendMCtx or mergeMCtx (10 messages, latest: Nov 08 2022 at 06:44)
- simp guard (18 messages, latest: Nov 07 2022 at 18:11)
- Propositions as Types and Antipatterns (6 messages, latest: Nov 07 2022 at 11:11)
- ✔ Macro expansion in tactics (1 message, latest: Nov 06 2022 at 19:29)
- ✔ Simple HEq (4 messages, latest: Nov 06 2022 at 19:16)
- lakefile dependencies (57 messages, latest: Nov 05 2022 at 23:41)
- Macro expansion in tactics (3 messages, latest: Nov 05 2022 at 22:27)
- dot notation seeing through defs (3 messages, latest: Nov 05 2022 at 08:32)
- ✔ Creating SyntaxNodeKinds for parsers (2 messages, latest: Nov 03 2022 at 23:03)
- Redundant alternative error (12 messages, latest: Nov 03 2022 at 22:56)
- ✔ Turn off all pretty printing and delaboration (8 messages, latest: Nov 03 2022 at 22:22)
- Macro using ← notation (10 messages, latest: Nov 03 2022 at 21:54)
- Ignore expected type for ▸ (26 messages, latest: Nov 03 2022 at 19:00)
- Writing parsers (11 messages, latest: Nov 03 2022 at 17:45)
- Semantics of repeat (9 messages, latest: Nov 03 2022 at 17:12)
- ✔ tactic to name variables with daggers (5 messages, latest: Nov 03 2022 at 14:31)
- negative squares (3 messages, latest: Nov 03 2022 at 09:19)
- Creating SyntaxNodeKinds for parsers (6 messages, latest: Nov 03 2022 at 01:52)
- Decidable of Exists changes
if
macro semantics (21 messages, latest: Nov 02 2022 at 20:27) - Hints for foundations for lemmas on Rat (41 messages, latest: Nov 02 2022 at 19:11)
- Stack trace profiling (37 messages, latest: Nov 02 2022 at 18:05)
- use cases of abbrev (4 messages, latest: Nov 02 2022 at 15:08)
- Gitpod (8 messages, latest: Nov 02 2022 at 11:27)
- Accessing environment during tests (6 messages, latest: Nov 02 2022 at 00:56)
- Can't get lean4 working with VS Code. (10 messages, latest: Nov 01 2022 at 23:03)
- Inferring the type of syntax during term elaboration (5 messages, latest: Nov 01 2022 at 23:00)
- motive is not type correct (9 messages, latest: Nov 01 2022 at 19:10)
- ✔ Benchmarking Tactics (1 message, latest: Nov 01 2022 at 18:20)
- Benchmarking Tactics (4 messages, latest: Nov 01 2022 at 18:18)
- Rpc error on hole in
cases with
tactic (8 messages, latest: Oct 31 2022 at 05:02) - Proving termination for Parsec (2 messages, latest: Oct 31 2022 at 04:23)
- closing Float
-0 = 0
(83 messages, latest: Oct 31 2022 at 04:19) - Lean 4 error: unknown package 'Leanpkg' (15 messages, latest: Oct 30 2022 at 20:23)
- Use a ConstructorVal in syntax as a constructor (5 messages, latest: Oct 30 2022 at 04:06)
- command-line arguments for Alectryon Sphinx extension (4 messages, latest: Oct 30 2022 at 01:19)
- Extending do notation with
+=
(18 messages, latest: Oct 30 2022 at 00:28) - Type mismatch with projection notation (2 messages, latest: Oct 30 2022 at 00:07)
- Q: Nat.any vs Nat.anyTR (5 messages, latest: Oct 29 2022 at 03:08)
- Unifying dependent types (11 messages, latest: Oct 28 2022 at 17:18)
- identify LeanInk exe (8 messages, latest: Oct 28 2022 at 01:34)
- implemented_by type error (3 messages, latest: Oct 27 2022 at 23:36)
- IR check failed when should be noncomputable (6 messages, latest: Oct 27 2022 at 12:51)
- ✔ elan toolchains broken on macos M1 (1 message, latest: Oct 27 2022 at 07:23)
- Building shared library depending on mathlib (1 message, latest: Oct 26 2022 at 17:07)
- Bug in kernel level normalization (11 messages, latest: Oct 26 2022 at 16:12)
- Separation Logic (2 messages, latest: Oct 26 2022 at 15:38)
- elan toolchains broken on macos M1 (17 messages, latest: Oct 26 2022 at 13:01)
- norm_cast not seeing coercion? (9 messages, latest: Oct 25 2022 at 22:55)
- how to tell if defs rely on partial defs? (13 messages, latest: Oct 25 2022 at 21:48)
- Efficient generated code (7 messages, latest: Oct 25 2022 at 11:23)
- ✔ ac_rfl example doesn't work (3 messages, latest: Oct 25 2022 at 08:28)
- Re-assembling a TSyntax `tacticSeq (32 messages, latest: Oct 25 2022 at 06:44)
- simp vs rw behavior with lemmas supplied by instances (4 messages, latest: Oct 25 2022 at 05:29)
- Lean 4 analogue with
decl_name
(4 messages, latest: Oct 24 2022 at 23:43) - Codata and Recursion scheme in Lean (2 messages, latest: Oct 24 2022 at 21:16)
- switch off markdown highlighting in comments (1 message, latest: Oct 24 2022 at 16:34)
- understanding simp and interaction with iff and hypotheses (9 messages, latest: Oct 24 2022 at 06:13)
- protected constructors (2 messages, latest: Oct 24 2022 at 05:43)
- Interpreter? (10 messages, latest: Oct 23 2022 at 14:28)
- ✔ How to lookup the precedence of a symbol? (8 messages, latest: Oct 23 2022 at 10:43)
- How to lookup the precedence of a symbol? (2 messages, latest: Oct 23 2022 at 10:14)
- ✔ What does dagger mean in code hint? (5 messages, latest: Oct 23 2022 at 10:10)
- nested ReaderT (22 messages, latest: Oct 23 2022 at 01:52)
- Implicit lambdas in inverse function (16 messages, latest: Oct 22 2022 at 20:12)
- Typeclass resolution with functions (1 message, latest: Oct 22 2022 at 17:06)
- elab
foo with x y
(21 messages, latest: Oct 22 2022 at 08:40) - ✔
lean4 install problemsreverting to lean3 (2 messages, latest: Oct 22 2022 at 04:31) - #print notation (16 messages, latest: Oct 21 2022 at 21:45)
- Type Inference Problem (3 messages, latest: Oct 21 2022 at 15:19)
- 10-20 update (16 messages, latest: Oct 21 2022 at 10:34)
Quot.lcInv
error withabbrev
(1 message, latest: Oct 21 2022 at 08:03)- name of coercion (6 messages, latest: Oct 21 2022 at 01:18)
- Lean.Elab.runFrontend without typechecking (17 messages, latest: Oct 21 2022 at 00:54)
- Eq.subst (6 messages, latest: Oct 20 2022 at 19:21)
lean4 install problemsreverting to lean3 (37 messages, latest: Oct 20 2022 at 18:36)- ✔ Typeclass inference failing (1 message, latest: Oct 20 2022 at 18:30)
- Boolean and/or etc (29 messages, latest: Oct 20 2022 at 18:17)
- Using ref in lean 4 (basic q) (19 messages, latest: Oct 20 2022 at 18:11)
- intro with type specified (8 messages, latest: Oct 20 2022 at 16:22)
- Port NNG to Lean 4 (151 messages, latest: Oct 20 2022 at 16:00)
- Namespacing a synonym lemma under a prefix (7 messages, latest: Oct 20 2022 at 13:24)
- Typeclass inference failing (3 messages, latest: Oct 20 2022 at 12:08)
- Checking the Goldbach conjecture (38 messages, latest: Oct 20 2022 at 09:19)
- ✔ inferType and expressions introduced by have (1 message, latest: Oct 19 2022 at 19:56)
- ✔ Iterate through Array with index (5 messages, latest: Oct 19 2022 at 18:05)
- Benefits of Lean 4 (12 messages, latest: Oct 19 2022 at 15:49)
- Jump to definition of notation (5 messages, latest: Oct 19 2022 at 09:10)
- minor linter issue (1 message, latest: Oct 19 2022 at 07:43)
- Editor panic (15 messages, latest: Oct 18 2022 at 21:15)
- absolute value (10 messages, latest: Oct 18 2022 at 20:11)
- Rewriting congruent relations (48 messages, latest: Oct 18 2022 at 17:51)
- lean4#1743 (19 messages, latest: Oct 18 2022 at 00:36)
- inferType and expressions introduced by have (4 messages, latest: Oct 17 2022 at 22:02)
- Typeclass resolution with type functions (7 messages, latest: Oct 17 2022 at 19:00)
- ✔ openDecl syntax (4 messages, latest: Oct 17 2022 at 08:09)
- ✔ Diamond problem with notation (1 message, latest: Oct 17 2022 at 07:26)
- Simplification of imax 1 u (5 messages, latest: Oct 17 2022 at 05:44)
- Error message in class argument (2 messages, latest: Oct 16 2022 at 22:15)
- Diamond problem with notation (2 messages, latest: Oct 16 2022 at 14:07)
- Show expanded macros (5 messages, latest: Oct 16 2022 at 13:48)
- Working with inequalities (11 messages, latest: Oct 15 2022 at 21:19)
- Functor Array (1 message, latest: Oct 15 2022 at 13:53)
- indent after have (46 messages, latest: Oct 15 2022 at 06:51)
- Issue with simp? (11 messages, latest: Oct 15 2022 at 06:36)
- Integer algebraic properties (4 messages, latest: Oct 15 2022 at 02:00)
- where is the lean4 core library defined? (3 messages, latest: Oct 14 2022 at 23:33)
- where is the lean4 core libary defined? (2 messages, latest: Oct 14 2022 at 23:17)
- how to deal with "motive / result is not type correct"? (1 message, latest: Oct 14 2022 at 14:19)
- Trouble in VS Code (9 messages, latest: Oct 14 2022 at 13:28)
- debug tactic 'apply' failed, failed to unify (12 messages, latest: Oct 14 2022 at 09:39)
- shorter cases tactic (82 messages, latest: Oct 14 2022 at 04:26)
- symmetry tactic (19 messages, latest: Oct 14 2022 at 00:55)
- Regression in function coercion inference (3 messages, latest: Oct 13 2022 at 22:53)
- working with universal typeclass instances (7 messages, latest: Oct 13 2022 at 17:08)
- ✔ Parsing with
apply
and indentation (6 messages, latest: Oct 13 2022 at 16:18) - building expressions with intermediate metavariables (12 messages, latest: Oct 13 2022 at 06:41)
- Deriving Add (23 messages, latest: Oct 12 2022 at 23:56)
- ✔ Subtypes and equality (2 messages, latest: Oct 12 2022 at 23:02)
- types of tombstoned hypotheses? (2 messages, latest: Oct 12 2022 at 22:55)
- copilot demo video (6 messages, latest: Oct 12 2022 at 19:03)
- incorporating std (7 messages, latest: Oct 12 2022 at 15:14)
- Contract for equality and Hashable? (12 messages, latest: Oct 12 2022 at 13:12)
- tracing in one file? (5 messages, latest: Oct 12 2022 at 08:36)
- analogue of
trace_state
(4 messages, latest: Oct 12 2022 at 08:33) - map Array while mutating state (8 messages, latest: Oct 12 2022 at 08:29)
- Subtypes and equality (2 messages, latest: Oct 11 2022 at 22:10)
- Testing commands help (3 messages, latest: Oct 11 2022 at 21:04)
- print kernel terms (4 messages, latest: Oct 11 2022 at 10:44)
- new build system for lean (9 messages, latest: Oct 11 2022 at 08:28)
- split tactic on AND ? (5 messages, latest: Oct 11 2022 at 01:35)
- heartbeats, GMP vs no GMP (25 messages, latest: Oct 10 2022 at 20:15)
- deriving Hashable on recursive inductive (7 messages, latest: Oct 10 2022 at 13:04)
- congr (4 messages, latest: Oct 10 2022 at 05:10)
- Annoying LCNF errors (17 messages, latest: Oct 09 2022 at 19:29)
- change in
simp
behaviour #2 (7 messages, latest: Oct 08 2022 at 14:52) - proofs about values in
do
notation (15 messages, latest: Oct 08 2022 at 09:09) - ✔ Mu symbol (2 messages, latest: Oct 08 2022 at 08:24)
- Lean Manual: Monads documentation question/suggestion (12 messages, latest: Oct 08 2022 at 08:22)
- Mu symbol (3 messages, latest: Oct 08 2022 at 08:18)
- Wrong version in VS Code (27 messages, latest: Oct 07 2022 at 20:10)
Cannot read properties of undefined
(28 messages, latest: Oct 07 2022 at 15:20)- HashMap moved to std (18 messages, latest: Oct 07 2022 at 14:05)
- Hole commands (2 messages, latest: Oct 07 2022 at 13:11)
- What is ST.Ref.take? (10 messages, latest: Oct 07 2022 at 08:32)
- Lean 4 analogue of semireducible for TransparencyMode? (15 messages, latest: Oct 07 2022 at 06:07)
- cc tactic (3 messages, latest: Oct 07 2022 at 02:27)
- ✔ Parser category for instance parameters (3 messages, latest: Oct 07 2022 at 01:30)
- root namespace with idents (13 messages, latest: Oct 07 2022 at 01:22)
- crash when using "by decide" (3 messages, latest: Oct 07 2022 at 00:12)
- unfolding earlier fields (3 messages, latest: Oct 06 2022 at 23:59)
- ✔ Defining non-reserved syntax (2 messages, latest: Oct 06 2022 at 21:37)
- Parser category for instance parameters (11 messages, latest: Oct 06 2022 at 14:15)
- Defining non-reserved syntax (2 messages, latest: Oct 06 2022 at 14:09)
- Function for taking apart applications (1 message, latest: Oct 06 2022 at 12:26)
- idiomatic replacement for pattern matching on expressions (14 messages, latest: Oct 06 2022 at 08:32)
- expr.of_nat (4 messages, latest: Oct 06 2022 at 06:15)
- Dot notation in syntax antiquotations (11 messages, latest: Oct 06 2022 at 03:52)
- enumerate (27 messages, latest: Oct 05 2022 at 21:58)
- Chaining commands defined as macros (10 messages, latest: Oct 05 2022 at 20:37)
- VSCode "Waiting for lean server to start…" (80 messages, latest: Oct 05 2022 at 19:08)
- private imports / private section (2 messages, latest: Oct 05 2022 at 14:59)
- doc-gen4 broken (208 messages, latest: Oct 05 2022 at 11:15)
- Return Prop by elimination of Or/Sum (4 messages, latest: Oct 05 2022 at 07:43)
- lean4 install problems (9 messages, latest: Oct 05 2022 at 07:17)
- Do Functors preserve identities? (12 messages, latest: Oct 04 2022 at 21:00)
- ✔ Extending structure, problem with
this
(1 message, latest: Oct 04 2022 at 19:26) - Extending structure, problem with
this
(3 messages, latest: Oct 04 2022 at 19:00) - Term reduction in type (34 messages, latest: Oct 04 2022 at 17:44)
- Command for making structures (5 messages, latest: Oct 04 2022 at 14:23)
- “mapsto” syntax for lambdas (4 messages, latest: Oct 03 2022 at 19:17)
- "have" with tactic-mode proof (45 messages, latest: Oct 03 2022 at 18:57)
- defining attributes (3 messages, latest: Oct 03 2022 at 18:13)
- issues extracting proofs (3 messages, latest: Oct 03 2022 at 17:27)
- Unification with free variables of structure type (4 messages, latest: Oct 03 2022 at 17:13)
- Recursive definition fails (3 messages, latest: Oct 02 2022 at 14:09)
- Why are implicit arguments inserted eagerly? (10 messages, latest: Oct 02 2022 at 08:53)
- Running tactics during instance synthesis (11 messages, latest: Oct 01 2022 at 21:29)
- Reasoning about Integers (4 messages, latest: Oct 01 2022 at 16:12)
- debugging 'apply' failed to unify (8 messages, latest: Oct 01 2022 at 14:16)
- Installing mathlib on M1 Mac (6 messages, latest: Sep 30 2022 at 23:57)
- lean4 version of le_add_comm (21 messages, latest: Sep 30 2022 at 20:55)
- Decidable fight (47 messages, latest: Sep 30 2022 at 16:23)
- ✔
let rec
inside proofs? (2 messages, latest: Sep 30 2022 at 15:28) - elabAselim issue (5 messages, latest: Sep 30 2022 at 14:11)
- VSCode does not react to changes (5 messages, latest: Sep 30 2022 at 11:36)
- ✔ lean4 version of le_add_comm (1 message, latest: Sep 29 2022 at 20:46)
- Universe issue when building expression (4 messages, latest: Sep 29 2022 at 19:27)
- Beginner question about typeclass constraints (28 messages, latest: Sep 29 2022 at 15:37)
- error when building Std (2 messages, latest: Sep 29 2022 at 13:52)
- [RFC] reunifying intro and intros (5 messages, latest: Sep 29 2022 at 09:45)
- disable linter in elab (17 messages, latest: Sep 28 2022 at 21:00)
- lake build updating manifest? (8 messages, latest: Sep 28 2022 at 19:57)
- Strange typechecking or parsing issue in lean4 (7 messages, latest: Sep 28 2022 at 17:36)
- Can't install nightly (3 messages, latest: Sep 28 2022 at 16:35)
- removing elements in vectors (20 messages, latest: Sep 28 2022 at 16:02)
- Type equality issue (14 messages, latest: Sep 28 2022 at 15:57)
- pattern matching with 'cases' and 'match' (14 messages, latest: Sep 28 2022 at 11:27)
- ✔ Structure extensionality (9 messages, latest: Sep 28 2022 at 10:36)
- Structure extensionality (1 message, latest: Sep 28 2022 at 07:49)
- ✔ Stateful/Aggregating Macros? (1 message, latest: Sep 28 2022 at 06:49)
- StateRefT (8 messages, latest: Sep 28 2022 at 01:19)
- modifiable state inside a ReaderM struct (120 messages, latest: Sep 28 2022 at 00:36)
- ✔ inline codegen crash (2 messages, latest: Sep 28 2022 at 00:09)
- Beginner questions about equalities (13 messages, latest: Sep 28 2022 at 00:01)
- LCNF local context contains unused local variable declaratio (2 messages, latest: Sep 27 2022 at 23:54)
- |> macro vs def (10 messages, latest: Sep 27 2022 at 21:33)
- inline codegen crash (15 messages, latest: Sep 27 2022 at 20:18)
- defeq sort and reassociation (3 messages, latest: Sep 27 2022 at 18:24)
let rec
inside proofs? (10 messages, latest: Sep 27 2022 at 17:41)- Stateful/Aggregating Macros? (5 messages, latest: Sep 27 2022 at 17:22)
- Metaprogramming MVars for case matching (4 messages, latest: Sep 27 2022 at 08:11)
- IO.waitAny but no IO.waitAll ? (6 messages, latest: Sep 27 2022 at 06:17)
- nix:
roots
forbuildLeanPackage
(6 messages, latest: Sep 26 2022 at 21:16) - lean-toolchain point to local build (3 messages, latest: Sep 26 2022 at 20:38)
- HashMap extension (28 messages, latest: Sep 26 2022 at 19:25)
- Computed Fields feature (37 messages, latest: Sep 26 2022 at 14:49)
- Go to definition not finding some definitions (22 messages, latest: Sep 26 2022 at 13:11)
- Expr: β-Reduction for ∏ binders? (4 messages, latest: Sep 26 2022 at 11:37)
- Mysterious import failure (5 messages, latest: Sep 26 2022 at 09:01)
- Good syntax/approach for small category theory example? (1 message, latest: Sep 25 2022 at 17:39)
- ✔ Installing lean4 via nix on arm mac (2 messages, latest: Sep 25 2022 at 12:58)
- Error in intros (9 messages, latest: Sep 24 2022 at 20:13)
- Tail recursive bind (6 messages, latest: Sep 23 2022 at 23:07)
- binders position info (15 messages, latest: Sep 23 2022 at 21:55)
- lean hanging mwe (8 messages, latest: Sep 23 2022 at 17:18)
- register_simp_attr requires a docstring? (5 messages, latest: Sep 22 2022 at 22:12)
- Referential transparency and proofs (5 messages, latest: Sep 22 2022 at 19:06)
- building with depencies (8 messages, latest: Sep 22 2022 at 15:50)
- lookup table (6 messages, latest: Sep 22 2022 at 07:56)
- ✔ instances of nat (2 messages, latest: Sep 22 2022 at 02:05)
- Syntax for a list of terms (4 messages, latest: Sep 21 2022 at 14:56)
- ✔ How to use
expandOptLocation
? (5 messages, latest: Sep 21 2022 at 11:50) - Custom parser (3 messages, latest: Sep 21 2022 at 10:34)
- brew elan missing nightly (8 messages, latest: Sep 21 2022 at 08:38)
- instances of nat (7 messages, latest: Sep 21 2022 at 06:29)
- precompileModules (39 messages, latest: Sep 21 2022 at 03:19)
- dot notation in a cases match (1 message, latest: Sep 20 2022 at 19:40)
- ✔ Extracting
inr
having a proof ofisInr
(2 messages, latest: Sep 20 2022 at 19:14) - Extracting
inr
having a proof ofisInr
(23 messages, latest: Sep 20 2022 at 19:13) - Lake default verbosity (10 messages, latest: Sep 20 2022 at 19:13)
- "does not have executable code" (1 message, latest: Sep 20 2022 at 12:21)
- Structure Extension Naming (1 message, latest: Sep 20 2022 at 09:21)
- List Functor (81 messages, latest: Sep 20 2022 at 06:34)
- ✔ Potential elaboration bug with
elabAsElim
(1 message, latest: Sep 20 2022 at 04:52) - ✔
isExclusive
function? (2 messages, latest: Sep 20 2022 at 03:53) - Forall vs. if-then (11 messages, latest: Sep 19 2022 at 18:13)
isExclusive
function? (3 messages, latest: Sep 19 2022 at 17:36)- Potential elaboration bug with
elabAsElim
(4 messages, latest: Sep 19 2022 at 14:17) - Installing lean4 via nix on arm mac (5 messages, latest: Sep 19 2022 at 12:11)
- ✔ And & Or over Type (5 messages, latest: Sep 19 2022 at 10:04)
- And & Or over Type (1 message, latest: Sep 19 2022 at 09:04)
- Discrimination tree lookup (16 messages, latest: Sep 19 2022 at 08:42)
- andThen operator (21 messages, latest: Sep 18 2022 at 22:12)
- Lean doc suggestion (8 messages, latest: Sep 18 2022 at 07:55)
- Identifier with number (3 messages, latest: Sep 17 2022 at 06:58)
- widget bug? (4 messages, latest: Sep 17 2022 at 03:35)
- ✔ Strangeness with bound variables (5 messages, latest: Sep 16 2022 at 19:40)
- Proving termination of monadic functions (6 messages, latest: Sep 16 2022 at 19:05)
- Mathlib dependency fails to build? (22 messages, latest: Sep 16 2022 at 17:15)
- ✔ [] vs #[] notation (4 messages, latest: Sep 16 2022 at 10:31)
- repeat' (18 messages, latest: Sep 16 2022 at 02:20)
- Learning lean macros (12 messages, latest: Sep 16 2022 at 00:40)
- [] vs #[] notation (6 messages, latest: Sep 15 2022 at 18:57)
- do block: invalid reassignment (10 messages, latest: Sep 15 2022 at 18:41)
- ✔ Export smart constructor but also the type (2 messages, latest: Sep 15 2022 at 17:22)
- reference type checker (5 messages, latest: Sep 15 2022 at 13:29)
assumption
as aTacticM Unit
(8 messages, latest: Sep 15 2022 at 04:12)- teaching early US ugrads f'22 (63 messages, latest: Sep 15 2022 at 02:43)
- Export smart constructor but also the type (6 messages, latest: Sep 15 2022 at 02:29)
- Structure with noncomputable rec/accessor? (8 messages, latest: Sep 14 2022 at 20:30)
- betaReduce with loose bvars (3 messages, latest: Sep 14 2022 at 12:13)
- parsing optional arguments (2 messages, latest: Sep 14 2022 at 07:35)
- Local definitions in mutual inductive type block (8 messages, latest: Sep 13 2022 at 20:53)
- 0 < 2 (12 messages, latest: Sep 13 2022 at 19:38)
- Equational Lemmas (10 messages, latest: Sep 13 2022 at 13:32)
- invalid pattern, constructor or constant marked with '[match (11 messages, latest: Sep 13 2022 at 00:44)
- Easily writing large Expr (17 messages, latest: Sep 12 2022 at 12:53)
- Array.partition vs Array.split (9 messages, latest: Sep 12 2022 at 06:39)
- dimensional analysis and arithmetic in type (11 messages, latest: Sep 11 2022 at 11:56)
- Help understanding GADTs (7 messages, latest: Sep 11 2022 at 07:18)
- lean for language specs (3 messages, latest: Sep 11 2022 at 02:54)
- ✔ Reasoning about monad transformer (1 message, latest: Sep 10 2022 at 11:45)
- One-bit Perceus (7 messages, latest: Sep 09 2022 at 20:20)
- Github Codespaces (1 message, latest: Sep 08 2022 at 23:48)
- a numerical lib for Lean 4 (100 messages, latest: Sep 08 2022 at 21:40)
- Unknown constant …._spec_N (3 messages, latest: Sep 08 2022 at 18:40)
- "Failed to elaborate eliminator" (4 messages, latest: Sep 08 2022 at 18:38)
- Tutorial for Scala programmers (3 messages, latest: Sep 08 2022 at 18:19)
- Antiquot Splice (9 messages, latest: Sep 08 2022 at 12:25)
- Lean4 LSP documentation? Want to make a "diagram chaser". (76 messages, latest: Sep 08 2022 at 03:54)
- ✔ lake target path (1 message, latest: Sep 08 2022 at 03:47)
- Function dot notation error (14 messages, latest: Sep 07 2022 at 22:24)
- lake target path (4 messages, latest: Sep 07 2022 at 18:13)
- ✔ Reader Monad porting (4 messages, latest: Sep 07 2022 at 18:08)
- have vs let (6 messages, latest: Sep 06 2022 at 23:56)
- Do we still need OptionM? (96 messages, latest: Sep 06 2022 at 16:15)
- Checkpointing subcommands (2 messages, latest: Sep 06 2022 at 09:59)
- Unexpected behavior of sorry (11 messages, latest: Sep 05 2022 at 18:27)
- ✔ Parser for a custom identifier (5 messages, latest: Sep 03 2022 at 18:51)
- Monads and Dependent Types (10 messages, latest: Sep 03 2022 at 14:59)
- Parser for a custom identifier (6 messages, latest: Sep 03 2022 at 14:08)
- can you do a safe cast to a subtype in Lean? (5 messages, latest: Sep 03 2022 at 13:06)
- How do I import a file? (19 messages, latest: Sep 03 2022 at 09:16)
- Reasoning about monad transformer (8 messages, latest: Sep 03 2022 at 08:46)
- Gitpod Lean 4 Samples (1 message, latest: Sep 02 2022 at 20:31)
- loop invariants (27 messages, latest: Sep 02 2022 at 09:09)
- Breaking changes in Lean 4 vs 3? (7 messages, latest: Sep 01 2022 at 19:28)
- BEq Subtype (22 messages, latest: Sep 01 2022 at 16:32)
- Force reduction of type (2 messages, latest: Sep 01 2022 at 14:57)
- ✔ Array.push Efficiency (8 messages, latest: Aug 31 2022 at 21:20)
- ✔ Question: strong normalization in Lean (6 messages, latest: Aug 31 2022 at 20:57)
- Question: strong normalization in Lean (4 messages, latest: Aug 31 2022 at 19:51)
- Hashable Subtype (5 messages, latest: Aug 31 2022 at 11:40)
- unknown package in lean4-samples (21 messages, latest: Aug 31 2022 at 03:21)
- monads documentation (23 messages, latest: Aug 30 2022 at 23:34)
- Debugging unification issues (8 messages, latest: Aug 30 2022 at 23:11)
- differentiation in SciLean (1 message, latest: Aug 30 2022 at 21:08)
- simp under binders (3 messages, latest: Aug 30 2022 at 19:31)
- Type inference errors on has_inner of a derived inner space (2 messages, latest: Aug 30 2022 at 16:55)
- Failed to show termination (16 messages, latest: Aug 30 2022 at 16:03)
- contradiction on bools (12 messages, latest: Aug 30 2022 at 14:57)
- List.index_of (29 messages, latest: Aug 30 2022 at 14:52)
- ✔ Phantom universe implicit (5 messages, latest: Aug 30 2022 at 13:03)
- Use local instance (8 messages, latest: Aug 30 2022 at 11:41)
- De-emphasizing inaccessible hypothesis names (19 messages, latest: Aug 30 2022 at 11:40)
lean --stdin
does not respect Ctrl+D (42 messages, latest: Aug 30 2022 at 05:20)- Anything like QuickCheck (5 messages, latest: Aug 30 2022 at 04:02)
- ✔ SeqLeft and SeqRight (1 message, latest: Aug 29 2022 at 20:32)
- ✔ Proving nonexistence of inductive fixpoints? (6 messages, latest: Aug 29 2022 at 11:41)
- Proving nonexistence of inductive fixpoints? (3 messages, latest: Aug 29 2022 at 10:11)
- Find
get!
panic source (6 messages, latest: Aug 28 2022 at 19:21) - Checking proper TC failure (2 messages, latest: Aug 28 2022 at 15:44)
- How to inspect attributes? (10 messages, latest: Aug 28 2022 at 09:06)
- what naming scheme to use in mathlib4 (13 messages, latest: Aug 27 2022 at 21:16)
- Custom error message for type classes (1 message, latest: Aug 27 2022 at 18:24)
- lifting transformers (18 messages, latest: Aug 27 2022 at 14:28)
- ✔ Meta: Debug values like #eval does? (4 messages, latest: Aug 27 2022 at 10:04)
- dumb questions (106 messages, latest: Aug 27 2022 at 08:09)
- string unification (6 messages, latest: Aug 26 2022 at 23:49)
- When to use withContext (6 messages, latest: Aug 26 2022 at 21:54)
- ✔ ac_refl and intro (4 messages, latest: Aug 26 2022 at 21:23)
- ✔
cases
elimination in tactic writing (11 messages, latest: Aug 26 2022 at 21:08) - ✔ Problem with high order unification (2 messages, latest: Aug 26 2022 at 20:50)
- how to return early (15 messages, latest: Aug 26 2022 at 15:42)
- Problem with high order unification (4 messages, latest: Aug 26 2022 at 15:19)
- ✔ inline extract value from monad (3 messages, latest: Aug 26 2022 at 15:18)
- backtrace for panic! (19 messages, latest: Aug 26 2022 at 12:49)
- Reader Monad porting (25 messages, latest: Aug 26 2022 at 09:33)
- Phantom universe implicit (4 messages, latest: Aug 26 2022 at 05:12)
- Design question (2 messages, latest: Aug 25 2022 at 21:37)
- ✔ universe coherence in
forall_3_true_iff
(22 messages, latest: Aug 25 2022 at 19:15) - SeqLeft and SeqRight (13 messages, latest: Aug 25 2022 at 18:39)
- mutually recursive instances (8 messages, latest: Aug 25 2022 at 15:55)
- Questions on dependent elimination failures (30 messages, latest: Aug 25 2022 at 13:33)
- inline extract value from monad (2 messages, latest: Aug 25 2022 at 13:05)
- Seq.seq on an Option (42 messages, latest: Aug 24 2022 at 23:58)
- deriving Repr for functions (3 messages, latest: Aug 24 2022 at 18:59)
- Naming for list lemmas (1 message, latest: Aug 24 2022 at 18:23)
- ac_refl and intro (4 messages, latest: Aug 24 2022 at 18:09)
- Is this a bug? (1 message, latest: Aug 24 2022 at 16:56)
- Extending tacticSeqs (2 messages, latest: Aug 24 2022 at 13:02)
- semantic highlighting doc (5 messages, latest: Aug 24 2022 at 06:52)
- ✔ Minor TPiL4 doc suggestion (7 messages, latest: Aug 23 2022 at 18:25)
- Syntax atoms beginning with a single quote (1 message, latest: Aug 23 2022 at 14:52)
- Lean.ConstantInfo.all strangeness (2 messages, latest: Aug 23 2022 at 14:27)
- Lake and 'cc' (16 messages, latest: Aug 23 2022 at 02:38)
- ✔ Updating parser from nightly-2022-03-11 (2 messages, latest: Aug 22 2022 at 23:19)
cases
elimination in tactic writing (7 messages, latest: Aug 22 2022 at 22:21)- Elaborate term with info view (12 messages, latest: Aug 22 2022 at 21:25)
- Updating parser from nightly-2022-03-11 (3 messages, latest: Aug 22 2022 at 20:08)
- elan, leanpkg and lake… I am lost (28 messages, latest: Aug 22 2022 at 17:56)
- structure-like custom syntax (6 messages, latest: Aug 22 2022 at 09:13)
- Minor TPiL4 doc suggestion (7 messages, latest: Aug 21 2022 at 20:19)
- Tactic simp term order (6 messages, latest: Aug 21 2022 at 18:42)
- ✔ #reduce does not terminate? (1 message, latest: Aug 21 2022 at 00:49)
- Lean Server stopped (9 messages, latest: Aug 20 2022 at 19:12)
- #reduce does not terminate? (15 messages, latest: Aug 20 2022 at 16:16)
- Destructor of Inductive Types (6 messages, latest: Aug 20 2022 at 15:27)
- Debuggin Evaluation (8 messages, latest: Aug 20 2022 at 12:03)
- Set up (21 messages, latest: Aug 20 2022 at 09:54)
- transparent instances (4 messages, latest: Aug 19 2022 at 12:42)
- question about monad type inference (50 messages, latest: Aug 18 2022 at 23:28)
- go to definition shortcut (5 messages, latest: Aug 18 2022 at 22:25)
- DocInk (45 messages, latest: Aug 18 2022 at 20:24)
- Default pattern with nested inductive (6 messages, latest: Aug 18 2022 at 09:55)
- missing MonadLift IO CommandElabM (4 messages, latest: Aug 18 2022 at 08:10)
- help with do notation (24 messages, latest: Aug 18 2022 at 02:31)
- ✔ Default value on recursive inductive error (11 messages, latest: Aug 17 2022 at 23:32)
- Recursive Structures (9 messages, latest: Aug 17 2022 at 23:24)
- Default value on recursive inductive error (1 message, latest: Aug 17 2022 at 18:50)
- recursive structures (1 message, latest: Aug 17 2022 at 17:49)
- [RFC] package.lean rename (14 messages, latest: Aug 17 2022 at 12:32)
- some graphical algorithm notation (19 messages, latest: Aug 16 2022 at 21:27)
- building multiple binaries (60 messages, latest: Aug 16 2022 at 14:29)
- C FFI export (86 messages, latest: Aug 16 2022 at 12:16)
- Required Internet Connection (4 messages, latest: Aug 16 2022 at 09:38)
- Expr.mdata (7 messages, latest: Aug 16 2022 at 07:19)
- Persistent extension not persisting (4 messages, latest: Aug 16 2022 at 06:26)
- Introduce ordering relation (9 messages, latest: Aug 16 2022 at 00:57)
- FYI: Automated Code Optimization with E-Graphs (3 messages, latest: Aug 15 2022 at 19:40)
- Dependent rewrite (6 messages, latest: Aug 15 2022 at 14:52)
- withSaveInfoContext (2 messages, latest: Aug 14 2022 at 21:12)
- Feature Request: Index with ranges (7 messages, latest: Aug 13 2022 at 20:49)
- How to reverse congr (5 messages, latest: Aug 12 2022 at 14:20)
- Overload notation (2 messages, latest: Aug 12 2022 at 14:09)
- Testing out widgets (10 messages, latest: Aug 12 2022 at 12:15)
- assert! with a custom message? (5 messages, latest: Aug 12 2022 at 00:52)
- 2nd Lean Dev Update Meeting (15 messages, latest: Aug 11 2022 at 20:21)
- Weird Lake errors (73 messages, latest: Aug 11 2022 at 20:18)
- ✔ Optional dependencies (2 messages, latest: Aug 11 2022 at 16:26)
- Optional dependencies (2 messages, latest: Aug 11 2022 at 16:09)
- UnionFind proof assistance (89 messages, latest: Aug 11 2022 at 15:43)
- 0 / 0 = -nan (30 messages, latest: Aug 11 2022 at 13:22)
- Mutual inductive + abbrev (6 messages, latest: Aug 11 2022 at 05:36)
- How to get and Use a copy of Mathlib in lean4? (3 messages, latest: Aug 11 2022 at 05:10)
- "function expected" with irreducible def (5 messages, latest: Aug 11 2022 at 02:46)
- Reflecting on type class instance search? (3 messages, latest: Aug 10 2022 at 20:50)
- VSCode Disable Output auto-focus (35 messages, latest: Aug 10 2022 at 08:43)
- Forcing Lake to build lib (26 messages, latest: Aug 10 2022 at 02:03)
- importModule (19 messages, latest: Aug 09 2022 at 15:54)
- ✔ Unnecessary Inhabited? (6 messages, latest: Aug 09 2022 at 14:43)
- Lean 4 as an application language (43 messages, latest: Aug 09 2022 at 09:51)
- Extension error message (26 messages, latest: Aug 09 2022 at 08:53)
- Nat.div_one in the standard library (2 messages, latest: Aug 08 2022 at 16:52)
- What is the best souce of documentation? (9 messages, latest: Aug 08 2022 at 13:22)
- [RFC] Hover doc strings (lean4#1443) (15 messages, latest: Aug 08 2022 at 09:32)
- Tactic regression tests via mathport (17 messages, latest: Aug 07 2022 at 19:27)
- Commenting tactic (48 messages, latest: Aug 07 2022 at 15:04)
- VS Code + Latex input usability (2 messages, latest: Aug 07 2022 at 05:20)
- [RFC] Attribute naming convention (8 messages, latest: Aug 06 2022 at 20:09)
- Parsec parser for decoding Uri escapes (35 messages, latest: Aug 06 2022 at 19:02)
- Shared mutable state (5 messages, latest: Aug 06 2022 at 18:08)
- ✔ C FFI: How to auto free pointer (1 message, latest: Aug 06 2022 at 17:20)
- Measure compute time (6 messages, latest: Aug 06 2022 at 12:48)
- Acces environment from command macro (80 messages, latest: Aug 06 2022 at 08:12)
- Macro for testing error messages (26 messages, latest: Aug 05 2022 at 18:07)
- Defining own Repr for an user-defined type (5 messages, latest: Aug 05 2022 at 16:41)
- nn game port (27 messages, latest: Aug 05 2022 at 15:09)
- Lean 4 as a scripting language in Houdini (16 messages, latest: Aug 05 2022 at 12:41)
- C FFI: How to auto free pointer (2 messages, latest: Aug 05 2022 at 11:08)
- ✔ conflicting namespaces in mutual declaration (4 messages, latest: Aug 05 2022 at 02:22)
- Another new member question (7 messages, latest: Aug 04 2022 at 22:37)
- New Member question about "Theorem Proving in Lean (6 messages, latest: Aug 04 2022 at 21:07)
- ✔ Subtleties of type class method argument plicity (5 messages, latest: Aug 04 2022 at 20:27)
- Data-level parallelism (20 messages, latest: Aug 04 2022 at 18:09)
- lean4-cli (8 messages, latest: Aug 04 2022 at 17:21)
- Subtleties of type class method argument plicity (1 message, latest: Aug 04 2022 at 17:18)
- Empty typeclasses and / or instances (4 messages, latest: Aug 03 2022 at 22:47)
- lean4-mode with nix-doom-emacs (18 messages, latest: Aug 03 2022 at 21:40)
- goal at the end of
simp at
(2 messages, latest: Aug 03 2022 at 16:28) - Possible bug from Elim0 on Fin (8 messages, latest: Aug 03 2022 at 00:03)
- ✔ partial recursive def: failed to show inhabited non empty (7 messages, latest: Aug 02 2022 at 21:24)
- ✔ sorry case infects whole function? (4 messages, latest: Aug 02 2022 at 16:04)
- sorry case infects whole function? (3 messages, latest: Aug 02 2022 at 15:14)
- Issue with linking (10 messages, latest: Aug 02 2022 at 14:21)
- Gym (4 messages, latest: Aug 02 2022 at 11:06)
- ✔ parametrizing modules: variable vs constant (i.e. opaque) (4 messages, latest: Aug 02 2022 at 10:42)
- parametrizing modules: variable vs constant (i.e. opaque) (2 messages, latest: Aug 02 2022 at 10:02)
- [how is
used in parsers?](topic/how.20is.20.3Cmissing.3E.20used.20in.20parsers.3F.html) (37 messages, latest: Aug 02 2022 at 08:47) - export structure field shorthand (3 messages, latest: Aug 02 2022 at 02:41)
- FYI: Thoughts on a broader Julia (Lean?) usage (29 messages, latest: Aug 02 2022 at 00:31)
- ✔ Typeclass instance with parametrized types (4 messages, latest: Aug 01 2022 at 15:40)
- Typeclass instance with parametrized types (3 messages, latest: Aug 01 2022 at 15:15)
- ✔ Branching depending on type equality (14 messages, latest: Aug 01 2022 at 14:03)
- ✔ What is inductive typeclass? (6 messages, latest: Aug 01 2022 at 13:53)
Lean.Elab.runFrontend
andimport Lean
(22 messages, latest: Aug 01 2022 at 13:27)- Expressing dedicated resource (1 message, latest: Aug 01 2022 at 12:26)
split
bug (1 message, latest: Jul 31 2022 at 22:13)- Bool from LT/LE (9 messages, latest: Jul 31 2022 at 18:29)
- How to fix "unknown package 'data'" for Lean 4 (1 message, latest: Jul 31 2022 at 10:36)
- ✔ Judging for the same constructor (6 messages, latest: Jul 31 2022 at 06:10)
- How to add a path in Lean exactly? (6 messages, latest: Jul 31 2022 at 04:27)
- How to fix "Waiting for Lean server to start…" for Lean 4 (1 message, latest: Jul 31 2022 at 03:05)
- ✔ FOL reasoning in Lean4 (6 messages, latest: Jul 30 2022 at 19:41)
- PHOAS example (2 messages, latest: Jul 30 2022 at 15:01)
- vectors in lean4 (149 messages, latest: Jul 30 2022 at 14:19)
- ✔ Custom errors during instance synthesis? (2 messages, latest: Jul 30 2022 at 14:01)
- Custom errors during instance synthesis? (10 messages, latest: Jul 30 2022 at 13:11)
- Submit Lean code on online judges (92 messages, latest: Jul 30 2022 at 05:36)
- FOL reasoning in Lean4 (29 messages, latest: Jul 30 2022 at 03:58)
- ✔ Addition to the flake template (2 messages, latest: Jul 30 2022 at 01:01)
- Addition to the flake template (4 messages, latest: Jul 29 2022 at 21:32)
whnf
is notwhnf
(22 messages, latest: Jul 29 2022 at 20:51)- partial recursive def: failed to show inhabited non empty (3 messages, latest: Jul 29 2022 at 11:27)
- dev setup for vscode: goto definition finds nightly (4 messages, latest: Jul 29 2022 at 08:11)
- IR check failed (18 messages, latest: Jul 29 2022 at 01:26)
- Character unicode code (9 messages, latest: Jul 28 2022 at 21:36)
- Calc mode (6 messages, latest: Jul 28 2022 at 18:17)
- ✔ VSCode Disable autocompletion on certain inputs (3 messages, latest: Jul 28 2022 at 09:10)
- numpy/jax etc? (13 messages, latest: Jul 28 2022 at 08:28)
- VSCode Disable autocompletion on certain inputs (1 message, latest: Jul 28 2022 at 08:18)
- ✔ How to assert at compile-time (17 messages, latest: Jul 28 2022 at 01:15)
- Rationals and Floats (3 messages, latest: Jul 27 2022 at 20:29)
- ✔ Metaprogramming tutorial on YouTube (4 messages, latest: Jul 27 2022 at 02:47)
- Metaprogramming tutorial on YouTube (1 message, latest: Jul 27 2022 at 01:05)
- How to match on
<\|>
syntax? (4 messages, latest: Jul 26 2022 at 20:06) - Function overloading issue (2 messages, latest: Jul 26 2022 at 14:16)
- deprecated tag (13 messages, latest: Jul 26 2022 at 13:06)
- ✔ Require monoid with well ordered underlying set (5 messages, latest: Jul 26 2022 at 12:45)
- Pretty printing Syntax fails (24 messages, latest: Jul 26 2022 at 11:03)
- Allowing antiquotes in custom syntax extensions? (15 messages, latest: Jul 26 2022 at 10:53)
- Finding leanshared.so (7 messages, latest: Jul 26 2022 at 04:08)
- Expaning a macro into a macro (3 messages, latest: Jul 26 2022 at 00:55)
- performance of equality with projections/mutual (7 messages, latest: Jul 25 2022 at 20:39)
- src/runtime/alloc.cpp linked list optimization (2 messages, latest: Jul 25 2022 at 17:19)
- Refactoring tool (7 messages, latest: Jul 25 2022 at 09:34)
- Indexed Inductive (3 messages, latest: Jul 25 2022 at 09:01)
- Macro defined recursively on Nat (5 messages, latest: Jul 24 2022 at 23:17)
- Only allowing certain numerals (2 messages, latest: Jul 24 2022 at 15:09)
- General Programming (24 messages, latest: Jul 24 2022 at 12:32)
- universe polymorphic IO (74 messages, latest: Jul 24 2022 at 10:32)
mut
arguments (15 messages, latest: Jul 23 2022 at 22:28)- Showing syntax in generated documentation (6 messages, latest: Jul 23 2022 at 12:53)
- constant, variable, parameter (8 messages, latest: Jul 22 2022 at 23:23)
- doc-gen4 feature request (93 messages, latest: Jul 22 2022 at 19:58)
- dot notation for class methods? (9 messages, latest: Jul 22 2022 at 15:29)
- when are struct field defaults evaluated? (4 messages, latest: Jul 22 2022 at 13:17)
- Json ser-deser (16 messages, latest: Jul 22 2022 at 12:53)
- Beginner questions (match expression) (39 messages, latest: Jul 22 2022 at 12:20)
- Dropping 'admit' (17 messages, latest: Jul 22 2022 at 08:34)
constructor
andApplicative
(16 messages, latest: Jul 22 2022 at 07:28)- ✔ Possible mistake in Theorem Proving online docs? (5 messages, latest: Jul 22 2022 at 04:56)
- Possible mistake in Theorem Proving online docs? (5 messages, latest: Jul 22 2022 at 03:41)
- ✔ Confusing syntax match (3 messages, latest: Jul 21 2022 at 21:52)
- parameter (21 messages, latest: Jul 21 2022 at 21:50)
- Confusing syntax match (6 messages, latest: Jul 21 2022 at 21:13)
- deriving DecidableEq in parametric inductive (2 messages, latest: Jul 21 2022 at 15:37)
- Custom instance deriving handlers (2 messages, latest: Jul 21 2022 at 15:35)
- until is a keyword? (5 messages, latest: Jul 21 2022 at 14:04)
- Naming condition (Prop) in while notation (2 messages, latest: Jul 21 2022 at 10:46)
- prove "bind" function is total (5 messages, latest: Jul 21 2022 at 01:38)
- ✔ class inductive? (1 message, latest: Jul 20 2022 at 18:16)
- class inductive? (7 messages, latest: Jul 20 2022 at 17:05)
- universe level maximum integer (7 messages, latest: Jul 20 2022 at 05:33)
- Total function not reducing (47 messages, latest: Jul 20 2022 at 04:04)
- ✔ Combining macros as functions (3 messages, latest: Jul 19 2022 at 09:39)
- Combining macros as functions (2 messages, latest: Jul 19 2022 at 09:12)
- IntellISense for Language Embeddings? (62 messages, latest: Jul 19 2022 at 08:52)
- ✔ Help with Inhabited (17 messages, latest: Jul 19 2022 at 00:45)
- structure with unassigned variable as default variable (24 messages, latest: Jul 19 2022 at 00:31)
- ✔ newtype (6 messages, latest: Jul 18 2022 at 20:43)
- Code style/formatting (2 messages, latest: Jul 18 2022 at 17:48)
- ✔ pattern matching sepBy syntax (4 messages, latest: Jul 18 2022 at 14:05)
- ToJson Float is missing? (4 messages, latest: Jul 18 2022 at 08:34)
- nightly updates (20 messages, latest: Jul 17 2022 at 20:09)
- easy metaprogramming questions (10 messages, latest: Jul 17 2022 at 19:14)
- Stack safe Bind (10 messages, latest: Jul 17 2022 at 17:26)
- Performance of terms after erasure (28 messages, latest: Jul 17 2022 at 13:47)
- tactic1 <|> tactic2 (7 messages, latest: Jul 16 2022 at 22:06)
- "do unchained" paper (15 messages, latest: Jul 16 2022 at 20:20)
- #eval (7 messages, latest: Jul 16 2022 at 19:46)
- Exploring the prelude (11 messages, latest: Jul 16 2022 at 19:42)
- five goals in infoview after cases (2 messages, latest: Jul 16 2022 at 19:23)
- instance DecidableEq ByteArray (4 messages, latest: Jul 15 2022 at 23:09)
- TC stuck on metavariable (5 messages, latest: Jul 15 2022 at 14:09)
- Performance issues when pattern matching (1 message, latest: Jul 15 2022 at 12:33)
- Eval's performance (3 messages, latest: Jul 15 2022 at 09:59)
- ✔ Pretty printing custom list literal (1 message, latest: Jul 15 2022 at 05:56)
- Pretty printing custom list literal (2 messages, latest: Jul 15 2022 at 02:23)
- Defining Vec as inductive with length as first argument (11 messages, latest: Jul 14 2022 at 23:00)
- Type checker performance (1 message, latest: Jul 14 2022 at 22:59)
- 1st Lean Dev Update Meeting (32 messages, latest: Jul 14 2022 at 22:59)
- ✔ Vector type doesn't reduce the natural number (2 messages, latest: Jul 14 2022 at 18:42)
- ✔ Type unification, structs and implicits (10 messages, latest: Jul 14 2022 at 17:17)
- Vector type doesn't reduce the natural number (3 messages, latest: Jul 14 2022 at 16:23)
- ✔ System time (9 messages, latest: Jul 14 2022 at 15:57)
- ✔ Multiparameter typeclasses mimicking textbook definitions (14 messages, latest: Jul 14 2022 at 15:03)
- Type unification, structs and implicits (12 messages, latest: Jul 14 2022 at 13:37)
- ✔ Interpret ByteArray as a String (7 messages, latest: Jul 14 2022 at 11:43)
- Lake uses a wrong commit (13 messages, latest: Jul 13 2022 at 21:42)
- Interpret ByteArray as a String (2 messages, latest: Jul 13 2022 at 21:13)
- lake clean (4 messages, latest: Jul 13 2022 at 19:14)
- Metaprogramming tutorial: custom assumption (5 messages, latest: Jul 13 2022 at 05:56)
- IO with a type parameter in universe > 1 (6 messages, latest: Jul 12 2022 at 21:21)
- VSCode: Where is semantic highlighting? (1 message, latest: Jul 12 2022 at 20:06)
- LSpec: A testing framework for Lean (58 messages, latest: Jul 12 2022 at 13:42)
- ✔ Porting Lean3 code to Lean4 with
Mathport
(2 messages, latest: Jul 12 2022 at 10:45) - Porting Lean3 code to Lean4 with
Mathport
(10 messages, latest: Jul 12 2022 at 10:10) - lake build not building dependency binary (10 messages, latest: Jul 12 2022 at 05:44)
- String.getOp (134 messages, latest: Jul 11 2022 at 21:38)
- lake : creating libraries that links with a shared object. (4 messages, latest: Jul 11 2022 at 18:31)
- Lean4 blog series (13 messages, latest: Jul 11 2022 at 04:45)
- Short array optimization experiment (34 messages, latest: Jul 10 2022 at 22:48)
- Non-regular inductive type and universes (6 messages, latest: Jul 10 2022 at 15:42)
- POption? (3 messages, latest: Jul 10 2022 at 06:13)
- ✔ Example of
have
expressions for proving termination (1 message, latest: Jul 09 2022 at 20:21) - Example of
have
expressions for proving termination (2 messages, latest: Jul 09 2022 at 19:58) - ✔ ac_refl with HAdd (5 messages, latest: Jul 09 2022 at 14:26)
- Type erasure (3 messages, latest: Jul 09 2022 at 13:18)
- unused let disappears (19 messages, latest: Jul 09 2022 at 00:59)
- Inline signatures vs signatures in let bindings (13 messages, latest: Jul 08 2022 at 14:41)
- Dealing with large computation (memory) (15 messages, latest: Jul 08 2022 at 14:25)
- conflicting namespaces in mutual declaration (3 messages, latest: Jul 07 2022 at 23:05)
- open type family with parameters (40 messages, latest: Jul 07 2022 at 20:11)
- unknown package Mathlib (17 messages, latest: Jul 07 2022 at 19:26)
- ✔ Rewrite under binder (1 message, latest: Jul 07 2022 at 18:27)
- Rewrite under binder (12 messages, latest: Jul 07 2022 at 18:04)
- lower case 'string' (14 messages, latest: Jul 07 2022 at 15:57)
- Have #print unfold definitions? (3 messages, latest: Jul 07 2022 at 13:29)
- Renaming "refresh file dependencies"? (19 messages, latest: Jul 07 2022 at 09:17)
- InfoView failing (10 messages, latest: Jul 06 2022 at 18:43)
- Mul.mul does not match operator for rewriting (4 messages, latest: Jul 06 2022 at 17:55)
- ✔ Definition of Nat in Lean4 library (1 message, latest: Jul 06 2022 at 17:39)
- Increase stack space (for Aesop) (9 messages, latest: Jul 06 2022 at 14:05)
- Viewing Syntax, Expr and IR (2 messages, latest: Jul 06 2022 at 13:45)
- Collapse cases (11 messages, latest: Jul 06 2022 at 08:22)
- Is code displayed at the infoview guaranteed to be well-typ? (3 messages, latest: Jul 06 2022 at 06:36)
- Relation between Meta/C++ typecheckers (12 messages, latest: Jul 06 2022 at 01:44)
- dependent products and equality (4 messages, latest: Jul 05 2022 at 20:34)
- runFrontend on a file with imports (18 messages, latest: Jul 05 2022 at 12:09)
- deterministic timeout with structures (6 messages, latest: Jul 04 2022 at 14:29)
- maximum recursion depth (1 message, latest: Jul 04 2022 at 14:07)
- Monadic graph algorithms (4 messages, latest: Jul 04 2022 at 14:03)
- Help with termination_by (6 messages, latest: Jul 04 2022 at 12:55)
- Computable fixpoint functors (1 message, latest: Jul 04 2022 at 08:08)
- case in dependent match not triggering (?) (6 messages, latest: Jul 03 2022 at 22:20)
- Compartmentalization of axioms in Lean 4 (61 messages, latest: Jul 03 2022 at 12:51)
- Ideas about a JS backend (14 messages, latest: Jul 03 2022 at 11:26)
- antiquot parsing (2 messages, latest: Jul 02 2022 at 18:16)
- Hi everyone 👋 (4 messages, latest: Jul 02 2022 at 04:00)
- How to have constraint on inductively defined type (8 messages, latest: Jul 02 2022 at 01:25)
- ✔ chained dot notation (1 message, latest: Jul 01 2022 at 23:57)
- chained dot notation (6 messages, latest: Jul 01 2022 at 20:33)
- ✔ tactics in terms (6 messages, latest: Jul 01 2022 at 20:16)
- ✔ type mismatch with identical types on named pattern match (3 messages, latest: Jul 01 2022 at 19:45)
- type mismatch with identical types on named pattern match (13 messages, latest: Jul 01 2022 at 19:09)
- WASM (4 messages, latest: Jul 01 2022 at 15:24)
- Generalizing let statement (9 messages, latest: Jul 01 2022 at 13:44)
- unfold essentially loops (3 messages, latest: Jul 01 2022 at 10:39)
- Naming Question [RFC?] (5 messages, latest: Jul 01 2022 at 10:36)
- intros; contradiction (1 message, latest: Jul 01 2022 at 07:33)
- emacs lean4-mode hanging (4 messages, latest: Jul 01 2022 at 03:27)
- Competitive programmers (41 messages, latest: Jul 01 2022 at 02:56)
- doc-gen4 linking specification (4 messages, latest: Jun 30 2022 at 18:16)
- lake tracing (3 messages, latest: Jun 30 2022 at 08:34)
- Typed Macro Issues? (4 messages, latest: Jun 30 2022 at 07:58)
- Quick Tour Video (2 messages, latest: Jun 30 2022 at 02:22)
- Where should SlimCheck/QuickCheck be? (6 messages, latest: Jun 29 2022 at 22:34)
- ✔ Putting bounds on List elements (6 messages, latest: Jun 29 2022 at 22:04)
- ✔ More on scoped syntax (3 messages, latest: Jun 29 2022 at 19:00)
- More on scoped syntax (1 message, latest: Jun 29 2022 at 17:39)
- Question about
InductiveVal
(3 messages, latest: Jun 29 2022 at 14:06) - (libc++abi) lean::exception: incomplete case (2 messages, latest: Jun 29 2022 at 13:58)
- 2 simple JSON questions (2 messages, latest: Jun 29 2022 at 13:14)
- Lean Assertion Violation (5 messages, latest: Jun 29 2022 at 07:38)
- include & omit (2 messages, latest: Jun 28 2022 at 21:24)
- lemma := theorem? (21 messages, latest: Jun 28 2022 at 20:37)
- raytracer (6 messages, latest: Jun 28 2022 at 19:38)
- Aesop update (31 messages, latest: Jun 28 2022 at 17:08)
- deterministic timeout (9 messages, latest: Jun 28 2022 at 16:39)
- ✔ Parametricity and Lean 4? (2 messages, latest: Jun 28 2022 at 07:50)
- lean-snakebird (2 messages, latest: Jun 27 2022 at 22:35)
- Namespace-based overloading does not find exports (21 messages, latest: Jun 27 2022 at 21:02)
- lake script API (9 messages, latest: Jun 27 2022 at 20:29)
- viper (1 message, latest: Jun 27 2022 at 18:40)
- simple binary naturals in Lean4 (47 messages, latest: Jun 27 2022 at 14:42)
- Distinguish dependet and nondependent
forallE
(5 messages, latest: Jun 27 2022 at 11:39) - mathport improvements for
data.num.add
(7 messages, latest: Jun 27 2022 at 07:29) - child process (2 messages, latest: Jun 27 2022 at 00:35)
- has_zero in lean4? (11 messages, latest: Jun 26 2022 at 18:06)
- Class params dependent on outParams (3 messages, latest: Jun 26 2022 at 17:17)
- Finger trees/polymorphic recursion (8 messages, latest: Jun 26 2022 at 17:15)
- Inconsistency vscode infoview with
induction ... with cas
(4 messages, latest: Jun 26 2022 at 16:30) - ✔ Newline-sensitive syntax (2 messages, latest: Jun 26 2022 at 14:21)
- Parametricity and Lean 4? (2 messages, latest: Jun 26 2022 at 09:00)
- Cabled arrow polynomials of virtual knots (7 messages, latest: Jun 26 2022 at 01:04)
- class dot notation (12 messages, latest: Jun 25 2022 at 20:15)
- ✔ Less than on natural numbers is an accessible relation (1 message, latest: Jun 25 2022 at 17:06)
- toNat? (6 messages, latest: Jun 25 2022 at 16:42)
- Less than on natural numbers is an accessible relation (15 messages, latest: Jun 25 2022 at 12:19)
- Newline-sensitive syntax (7 messages, latest: Jun 25 2022 at 11:10)
- ✔ Parsing C-style octal number (2 messages, latest: Jun 25 2022 at 08:12)
- Parsing C-style octal number (2 messages, latest: Jun 25 2022 at 06:19)
- "Fail to show termination" in merge sort implementation (31 messages, latest: Jun 24 2022 at 22:36)
- Lake's package vs lean_lib vs lean_exe (48 messages, latest: Jun 24 2022 at 22:33)
- Typed Macros (5 messages, latest: Jun 24 2022 at 21:58)
- How to know if a function is recursive? (13 messages, latest: Jun 24 2022 at 21:07)
- commandElab behaving weirdly (12 messages, latest: Jun 24 2022 at 13:07)
- How to get input from keyboard? (13 messages, latest: Jun 24 2022 at 07:29)
- Univerally quantified type class expression (1 message, latest: Jun 23 2022 at 15:15)
- empty universe levels (4 messages, latest: Jun 23 2022 at 12:58)
- Logic and Proof (5 messages, latest: Jun 23 2022 at 11:20)
- IO Mutable Array (22 messages, latest: Jun 23 2022 at 08:05)
- Rewriting modulo let (6 messages, latest: Jun 23 2022 at 02:42)
- Two Types of Inling? (4 messages, latest: Jun 23 2022 at 02:03)
- ✔ Forced implicit argument (9 messages, latest: Jun 22 2022 at 19:50)
- ✔ When to use 'opaque'? (5 messages, latest: Jun 22 2022 at 17:12)
- category theory code (9 messages, latest: Jun 22 2022 at 15:31)
- Unused variables linter (31 messages, latest: Jun 21 2022 at 18:35)
- Stack Overflow (6 messages, latest: Jun 21 2022 at 18:19)
- What is
_obj
? (2 messages, latest: Jun 21 2022 at 16:58) - Linux setups (55 messages, latest: Jun 21 2022 at 16:03)
- def vs abbrev (4 messages, latest: Jun 21 2022 at 15:53)
exact
works, but term mode fails (16 messages, latest: Jun 21 2022 at 15:49)- ✔ def vs abbrev (6 messages, latest: Jun 21 2022 at 11:40)
- Rewriting in a let-body (8 messages, latest: Jun 21 2022 at 10:49)
- safe/unsafe constants (4 messages, latest: Jun 21 2022 at 09:45)
- Monad over prop? (14 messages, latest: Jun 21 2022 at 04:17)
- Matching Recursive Subtypes (11 messages, latest: Jun 21 2022 at 01:18)
- When does Repr not work? (8 messages, latest: Jun 21 2022 at 00:58)
- Constructing Syntax (6 messages, latest: Jun 20 2022 at 17:38)
- ✔ simple universe question (5 messages, latest: Jun 20 2022 at 15:39)
- mutual theorems (11 messages, latest: Jun 20 2022 at 12:29)
- ✔ Override notation in local namespace (4 messages, latest: Jun 19 2022 at 18:46)
- Implication vs. Universal Quantification (8 messages, latest: Jun 19 2022 at 18:23)
- Incorrect
fun {a}
linter (1 message, latest: Jun 19 2022 at 13:17) - ✔ checking for
sorryAx
in elaborated terms (5 messages, latest: Jun 19 2022 at 12:10) - checking for
sorryAx
in elaborated terms (5 messages, latest: Jun 19 2022 at 11:03) - cade21 paper macro question (4 messages, latest: Jun 18 2022 at 19:40)
- Lost in the multiverse … (20 messages, latest: Jun 18 2022 at 17:30)
- Defining syntax (30 messages, latest: Jun 18 2022 at 12:32)
- ✔ Is Expr.isEq correct? (1 message, latest: Jun 18 2022 at 00:14)
- ✔ Metaprogramming with Expr.isProp (2 messages, latest: Jun 17 2022 at 21:38)
- Is Expr.isEq correct? (2 messages, latest: Jun 17 2022 at 21:12)
- Metaprogramming with Expr.isProp (2 messages, latest: Jun 17 2022 at 20:56)
- ✔ Prop Structure (2 messages, latest: Jun 17 2022 at 09:19)
- metaprogramming: how to create function with structural rec? (10 messages, latest: Jun 17 2022 at 08:09)
- Expr antiquotations (14 messages, latest: Jun 16 2022 at 21:43)
- Prop Structure (7 messages, latest: Jun 16 2022 at 21:15)
- Configuring Lakefile for multiple c files over the FFI (7 messages, latest: Jun 16 2022 at 17:52)
- What's needed for mutual defs? (31 messages, latest: Jun 16 2022 at 07:36)
- Multiple use of variables in syntax quotations (2 messages, latest: Jun 15 2022 at 23:24)
- Arrays in lean runtime (11 messages, latest: Jun 15 2022 at 08:02)
- ✔ updating lake (2 messages, latest: Jun 15 2022 at 07:33)
- updating lake (3 messages, latest: Jun 15 2022 at 07:10)
- Imports (27 messages, latest: Jun 15 2022 at 03:49)
- ✔ anonymous constructor inconsistency (7 messages, latest: Jun 15 2022 at 03:24)
- anonymous constructor inconsistency (5 messages, latest: Jun 14 2022 at 22:43)
- Proposal to separate elaboration from adding declarations (6 messages, latest: Jun 14 2022 at 21:51)
- Lean tossing an error over having exactly what it wants (14 messages, latest: Jun 14 2022 at 18:16)
- aliasing complex terms (5 messages, latest: Jun 14 2022 at 14:54)
- how to fill metavariables when compiling function in command (6 messages, latest: Jun 14 2022 at 10:07)
- [nightly] exunique problems (28 messages, latest: Jun 12 2022 at 20:17)
- Automation (56 messages, latest: Jun 12 2022 at 14:51)
- beginner's problem [nightly] (33 messages, latest: Jun 12 2022 at 08:30)
- Server Filename Windows Bug (3 messages, latest: Jun 11 2022 at 21:57)
- LeanInk (or Lean?) bug (7 messages, latest: Jun 11 2022 at 10:33)
- ✔ many lake fustrations (14 messages, latest: Jun 11 2022 at 08:14)
- ✔mathlib (125 messages, latest: Jun 11 2022 at 00:14)
- ✔ mismatch between (a: String) and String (7 messages, latest: Jun 10 2022 at 21:24)
- type-safe HTML: syntax vs elaboration? (5 messages, latest: Jun 10 2022 at 18:44)
- First release of "Functional Programming in Lean" (24 messages, latest: Jun 10 2022 at 06:59)
- ✔ FFI : m_foreach in lean_external_class (5 messages, latest: Jun 10 2022 at 04:02)
- FFI : m_foreach in lean_external_class (3 messages, latest: Jun 10 2022 at 02:25)
- ✔ mutually recursive syntax (9 messages, latest: Jun 09 2022 at 16:42)
- Slow(er) compilation with large inductive (13 messages, latest: Jun 09 2022 at 16:26)
- congr and forward dependencies (27 messages, latest: Jun 09 2022 at 10:59)
- exists in hypothesis (30 messages, latest: Jun 09 2022 at 07:36)
- VS Code lean server crash (10 messages, latest: Jun 08 2022 at 22:21)
- Converting structures from lean4 to C (16 messages, latest: Jun 08 2022 at 19:29)
- ✔ tagless final (simple) type inference (4 messages, latest: Jun 08 2022 at 16:01)
- tagless final (simple) type inference (3 messages, latest: Jun 08 2022 at 13:27)
- Local functions in instances (3 messages, latest: Jun 08 2022 at 10:43)
- ✔ antiquotations in docstrings (5 messages, latest: Jun 07 2022 at 15:44)
- ✔ Lists with predicates and proof erasure (1 message, latest: Jun 07 2022 at 15:18)
- antiquotations in docstrings (1 message, latest: Jun 07 2022 at 14:49)
- Lists with predicates and proof erasure (11 messages, latest: Jun 07 2022 at 03:31)
- ✔ File/folder structure vs namespaces (13 messages, latest: Jun 07 2022 at 02:38)
- Getting Started with Lean4 Video (3 messages, latest: Jun 07 2022 at 00:34)
- File/folder structure vs namespaces (1 message, latest: Jun 06 2022 at 18:03)
- Lean 4 HoTT Library (1 message, latest: Jun 06 2022 at 14:02)
- Failure to elab a match statement in a command (3 messages, latest: Jun 06 2022 at 11:13)
- ✔ Expected term error (9 messages, latest: Jun 05 2022 at 23:39)
- mutually recursive syntax (10 messages, latest: Jun 05 2022 at 17:36)
- Custom induction hypothesis (10 messages, latest: Jun 04 2022 at 15:00)
- use cases of custom attributes (12 messages, latest: Jun 04 2022 at 12:57)
- What exactly are double backticks (8 messages, latest: Jun 04 2022 at 07:33)
- Reflexive inductives (3 messages, latest: Jun 04 2022 at 04:10)
- What is
opaque
? (15 messages, latest: Jun 03 2022 at 20:01) - Open Documentation View (11 messages, latest: Jun 03 2022 at 19:43)
- ✔ Hygenic expansion in tactic gives the same name twice? (5 messages, latest: Jun 03 2022 at 16:07)
- Term Macro Docstrings (8 messages, latest: Jun 03 2022 at 14:32)
- ✔ Prove about do block (9 messages, latest: Jun 03 2022 at 09:50)
- Bootstrapping (5 messages, latest: Jun 03 2022 at 07:41)
- Exotic error behaviour? (5 messages, latest: Jun 02 2022 at 15:46)
- different dbg_traces (41 messages, latest: Jun 02 2022 at 09:16)
- (kernel) function expected .noConfusion (2 messages, latest: Jun 02 2022 at 01:00)
- ✔ Name → Syntax (3 messages, latest: Jun 01 2022 at 19:56)
- Lean.Expr.proj (17 messages, latest: Jun 01 2022 at 08:13)
- ✔ bind for indexed monad is "wrong" (2 messages, latest: May 31 2022 at 21:22)
- bind for indexed monad is "wrong" (3 messages, latest: May 31 2022 at 20:02)
- Syntax-aware document editing (8 messages, latest: May 31 2022 at 16:06)
- Define Macro (12 messages, latest: May 31 2022 at 14:09)
- Incorrect number of universe levels parameters (2 messages, latest: May 30 2022 at 13:46)
- Structural Recursion Problem (9 messages, latest: May 29 2022 at 08:11)
- ✔ Define Macro (3 messages, latest: May 28 2022 at 20:55)
- ✔ Enum Macro (3 messages, latest: May 28 2022 at 18:28)
- Enum Macro (8 messages, latest: May 28 2022 at 17:56)
- ✔ Should String.reverse be added? (1 message, latest: May 28 2022 at 17:36)
- contrapose (13 messages, latest: May 28 2022 at 15:35)
- exists unique (2 messages, latest: May 28 2022 at 08:33)
- struggling with a proof (26 messages, latest: May 28 2022 at 01:28)
- Causal profiling (4 messages, latest: May 27 2022 at 21:07)
- Try tactic (4 messages, latest: May 27 2022 at 15:08)
- Should String.reverse be added? (22 messages, latest: May 27 2022 at 13:51)
- ✔ Order of data type definition and usage does not match ? (2 messages, latest: May 27 2022 at 09:44)
- "Rewrite" with inequalities (13 messages, latest: May 27 2022 at 05:31)
- simple interactive unit testing? (10 messages, latest: May 27 2022 at 05:26)
- Lean.Elab.admitGoal is not noisy (3 messages, latest: May 26 2022 at 23:32)
- ✔ lean.exe no output, self-compiled, Windows MSYS (15 messages, latest: May 26 2022 at 21:12)
- elan breaks every now and then (2 messages, latest: May 26 2022 at 19:10)
- Semantic token "property" (3 messages, latest: May 26 2022 at 16:58)
- Tooling: What does semantic highlighting? (3 messages, latest: May 26 2022 at 12:31)
- Defining & using attributes in the same file? (5 messages, latest: May 26 2022 at 10:10)
- (kernel) unknown constant (3 messages, latest: May 26 2022 at 03:39)
- Probably a bug (5 messages, latest: May 26 2022 at 03:07)
- Ambiguous braces (26 messages, latest: May 26 2022 at 02:21)
- Proving from a negation (6 messages, latest: May 25 2022 at 22:35)
- Mutual records + inductives (5 messages, latest: May 25 2022 at 06:59)
- Getting string expression out of String.mk app (7 messages, latest: May 24 2022 at 18:13)
- ✔ Local bindings as syntactic abbreviations (2 messages, latest: May 24 2022 at 07:26)
- Local bindings as syntactic abbreviations (5 messages, latest: May 24 2022 at 06:25)
- Termination check not preserved under let binding. (2 messages, latest: May 23 2022 at 20:45)
- Split Decidable goal (5 messages, latest: May 23 2022 at 20:12)
- Match vs. Let Pattern (6 messages, latest: May 23 2022 at 19:30)
- Finite Sets (18 messages, latest: May 23 2022 at 16:54)
- Reading floats (6 messages, latest: May 23 2022 at 14:41)
- ✔ Different namespace for mutual inductive types (1 message, latest: May 23 2022 at 07:16)
- Match doesn't work when generating inductive via metaprogram (2 messages, latest: May 22 2022 at 13:51)
- ✔ command to generate universe polymorphic inductive failing (2 messages, latest: May 22 2022 at 10:07)
- command to generate universe polymorphic inductive failing (9 messages, latest: May 22 2022 at 08:45)
- Different namespace for mutual inductive types (4 messages, latest: May 22 2022 at 04:58)
- ✔ Theorem Proving in Lean 4 Document (8 messages, latest: May 21 2022 at 13:04)
- command loop (4 messages, latest: May 20 2022 at 22:24)
- Unexpected behavior of simp with pre lemma (1 message, latest: May 20 2022 at 22:01)
- ✔ Definition Macro? (11 messages, latest: May 20 2022 at 18:17)
- ✔ Detecting match case unreachability (3 messages, latest: May 20 2022 at 17:53)
- ✔ Using let rec in expansion produces error (3 messages, latest: May 20 2022 at 16:47)
- Detecting match case unreachability (4 messages, latest: May 20 2022 at 16:00)
- Using let rec in expansion produces error (1 message, latest: May 20 2022 at 15:55)
- redefining def (12 messages, latest: May 20 2022 at 14:30)
- @[eliminator] usage (2 messages, latest: May 20 2022 at 13:56)
- Definition Macro? (22 messages, latest: May 20 2022 at 13:51)
- ✔ VSCode server crashes on unusual paths (2 messages, latest: May 20 2022 at 13:45)
- macro problem (5 messages, latest: May 20 2022 at 13:04)
- VSCode server crashes on unusual paths (12 messages, latest: May 20 2022 at 11:14)
- macro escape syntax (2 messages, latest: May 20 2022 at 08:48)
- inductive type with dependent recursive substructure (11 messages, latest: May 19 2022 at 22:32)
- ✔ macro problem (16 messages, latest: May 19 2022 at 16:38)
- structure inheritance coercions/aliases? (5 messages, latest: May 19 2022 at 01:51)
- Negative lookahead syntax (13 messages, latest: May 18 2022 at 11:16)
- universes (49 messages, latest: May 18 2022 at 09:12)
- (kernel) declaration has metavariables (11 messages, latest: May 18 2022 at 07:48)
- forward declarations (7 messages, latest: May 17 2022 at 23:19)
- Order of data type definition and usage does not match ? (6 messages, latest: May 17 2022 at 23:08)
- scripted vs compiled code (9 messages, latest: May 17 2022 at 19:54)
- ✔ breaking compilation from a command (6 messages, latest: May 17 2022 at 14:14)
- infinite lists (29 messages, latest: May 17 2022 at 13:19)
- Custom pre/post methods in simp (4 messages, latest: May 16 2022 at 21:22)
- Predictable meta numbering? (7 messages, latest: May 15 2022 at 15:04)
- simp_all_arith weakness (2 messages, latest: May 14 2022 at 17:45)
- naming
macro_rules
expansion function (11 messages, latest: May 14 2022 at 17:21) - hypothesis can't be used (62 messages, latest: May 14 2022 at 10:26)
- BinderInfo and reduction (4 messages, latest: May 14 2022 at 08:41)
- mutual inductive and structure (6 messages, latest: May 13 2022 at 18:31)
- PrettyPrinter (38 messages, latest: May 13 2022 at 16:57)
- Unification with let bindings (3 messages, latest: May 13 2022 at 16:20)
- conv implicit args (1 message, latest: May 13 2022 at 15:40)
- Nontermination when reducing floats (5 messages, latest: May 13 2022 at 15:00)
- ✔ Leading dot syntax bug? (6 messages, latest: May 12 2022 at 09:35)
- Propositional irrelevance confusion (1 message, latest: May 12 2022 at 01:17)
- creating my own programming language in Lean (82 messages, latest: May 11 2022 at 14:11)
- ✔ Overloading for non-number syntax? (2 messages, latest: May 11 2022 at 13:54)
- Overloading for non-number syntax? (11 messages, latest: May 11 2022 at 13:31)
- numbers in names (7 messages, latest: May 11 2022 at 12:00)
- In buffer message alignment in lean4-mode (14 messages, latest: May 11 2022 at 10:24)
- Heterogenous operation and literals (53 messages, latest: May 11 2022 at 04:45)
- Constructing forall/exists syntax (5 messages, latest: May 10 2022 at 09:18)
- ✔ Regression in coercion inference (1 message, latest: May 10 2022 at 07:25)
- Regression in coercion inference (5 messages, latest: May 10 2022 at 01:54)
- ✔ indexed inductive types overwhelming server (4 messages, latest: May 09 2022 at 13:11)
- Order of definitions strange interaction with universes (9 messages, latest: May 09 2022 at 12:43)
- indexed inductive types overwhelming server (3 messages, latest: May 09 2022 at 08:39)
- ✔ Left recursion in tactic syntax definition (6 messages, latest: May 08 2022 at 19:39)
- Highlighting goals/hypotheses (1 message, latest: May 08 2022 at 15:01)
- ✔ failed to synthesize instance (5 messages, latest: May 08 2022 at 13:16)
- ✔ Custom default recursors? (2 messages, latest: May 07 2022 at 22:15)
- Custom default recursors? (2 messages, latest: May 07 2022 at 20:26)
- ✔ Ignoring hygiene for a single name (4 messages, latest: May 07 2022 at 13:42)
- Can I use Lean 4 to construct operations via groups, ring… (2 messages, latest: May 07 2022 at 12:43)
- Syntactic discrepancies on comma-separated lists (35 messages, latest: May 07 2022 at 12:40)
- proving DecidableEq for inductives (7 messages, latest: May 07 2022 at 00:17)
- ✔ Behavior of unknown identifier error (1 message, latest: May 06 2022 at 10:55)
- Behavior of unknown identifier error (5 messages, latest: May 06 2022 at 09:33)
- #eval with native functions (14 messages, latest: May 05 2022 at 20:05)
- autoImplicit confusion? (10 messages, latest: May 04 2022 at 22:06)
- Setting Elan to Specific version (3 messages, latest: May 04 2022 at 15:41)
- Inaccessible name bug (3 messages, latest: May 04 2022 at 15:14)
- 'unreachable' code was reached by termination check (3 messages, latest: May 04 2022 at 15:11)
- Implementing a tactic modifier (6 messages, latest: May 04 2022 at 05:38)
- better way of union type? (73 messages, latest: May 03 2022 at 22:55)
- The line between term elaboration and macro (2 messages, latest: May 03 2022 at 08:33)
- ✔ Can't provide impl for structure accessor? (7 messages, latest: May 02 2022 at 15:59)
- Can't provide impl for structure accessor? (4 messages, latest: May 02 2022 at 15:05)
- ✔ Problems with the Dependent cartesian product example (8 messages, latest: May 02 2022 at 14:52)
- Problems with the Dependent cartesian product example (2 messages, latest: May 02 2022 at 10:15)
- ✔ parenthesize: uncaught backtrack exception (2 messages, latest: May 02 2022 at 02:00)
- ✔ Focus on case without closing it (3 messages, latest: May 01 2022 at 14:43)
- Focus on case without closing it (3 messages, latest: May 01 2022 at 13:04)
- parenthesize: uncaught backtrack exception (6 messages, latest: May 01 2022 at 09:54)
- Cannot inherit constraint type class (12 messages, latest: May 01 2022 at 00:16)
- ✔ Tactic mode for mergesort (9 messages, latest: Apr 30 2022 at 22:23)
- Cannot rewrite term being cased on (28 messages, latest: Apr 30 2022 at 17:12)
- synthetic vs non synthetic meta variables (2 messages, latest: Apr 30 2022 at 17:01)
- printing floats (4 messages, latest: Apr 30 2022 at 00:51)
- ✔ Parser descriptor and orelse with two symbols (2 messages, latest: Apr 29 2022 at 21:50)
- Parser descriptor and orelse with two symbols (4 messages, latest: Apr 29 2022 at 21:11)
- Obtaining types of structure fields fields (6 messages, latest: Apr 29 2022 at 12:14)
- lake failing with git error (7 messages, latest: Apr 29 2022 at 03:37)
- how to test lean code (4 messages, latest: Apr 28 2022 at 14:33)
- Workaround for
{}
annotation in structures (15 messages, latest: Apr 28 2022 at 13:10) - How to make custom state monad (7 messages, latest: Apr 27 2022 at 23:19)
- How to prove theorems that use
cast
(17 messages, latest: Apr 27 2022 at 19:16) - antiquot bug (6 messages, latest: Apr 27 2022 at 08:41)
- ✔ simp uses incorrect theorem (13 messages, latest: Apr 27 2022 at 01:02)
- ✔ Abysmal performance when doing large inductions (1 message, latest: Apr 26 2022 at 21:52)
- On the implementation of attributes in doc-gen (26 messages, latest: Apr 26 2022 at 21:39)
- Explicit constructor arguments become implicit (3 messages, latest: Apr 26 2022 at 20:47)
- Abysmal performance when doing large inductions (59 messages, latest: Apr 26 2022 at 16:18)
- failed to generate equality theorems (7 messages, latest: Apr 26 2022 at 09:33)
- ✔ Missing named arg error reported late (2 messages, latest: Apr 26 2022 at 02:08)
- ✔ Extending
exists
? (5 messages, latest: Apr 25 2022 at 23:52) - Missing named arg error reported late (2 messages, latest: Apr 25 2022 at 23:33)
- Extending
exists
? (7 messages, latest: Apr 25 2022 at 23:13) - Linear algebra with Eigen (1 message, latest: Apr 25 2022 at 21:28)
- is this normal? (25 messages, latest: Apr 25 2022 at 18:34)
- ✔ macro expander (2 messages, latest: Apr 25 2022 at 09:42)
- Lake target to run cmake (5 messages, latest: Apr 25 2022 at 02:26)
- Forcing return type to be
size_t
(4 messages, latest: Apr 24 2022 at 19:23) - syntax for dependently typed structures with default values (4 messages, latest: Apr 24 2022 at 17:41)
- macro expander (3 messages, latest: Apr 24 2022 at 08:17)
- Agda to Lean translation issue (37 messages, latest: Apr 24 2022 at 04:04)
- type mismatch when assigning motive (8 messages, latest: Apr 22 2022 at 20:50)
- ✔ Agda to Lean translation issue (3 messages, latest: Apr 21 2022 at 21:46)
- ✔ error creating a macro for a tactic (5 messages, latest: Apr 21 2022 at 17:30)
- ✔ Wait this is valid? (4 messages, latest: Apr 21 2022 at 17:21)
- error creating a macro for a tactic (1 message, latest: Apr 21 2022 at 17:13)
- ✔ Failed to syntesize
OfNat
instance when pattern matching (5 messages, latest: Apr 21 2022 at 14:10) - ✔ Messing up Option's Coe (4 messages, latest: Apr 21 2022 at 13:43)
- Messing up Option's Coe (1 message, latest: Apr 21 2022 at 13:27)
- Lean4 package/code discovery (6 messages, latest: Apr 21 2022 at 11:34)
- Wait this is valid? (6 messages, latest: Apr 21 2022 at 10:38)
- ✔ Simp lemma collection (6 messages, latest: Apr 21 2022 at 00:20)
- strange error with unrelated theorem (12 messages, latest: Apr 20 2022 at 17:51)
- Pretty-printing universal quantifier (2 messages, latest: Apr 20 2022 at 17:10)
- mutual inductive and def (47 messages, latest: Apr 19 2022 at 16:42)
- ✔ Fintype elements (3 messages, latest: Apr 19 2022 at 13:13)
- Fintype elements (1 message, latest: Apr 19 2022 at 09:03)
- ✔ Confusing performance issues with induction (3 messages, latest: Apr 18 2022 at 23:20)
- Confusing performance issues with induction (5 messages, latest: Apr 18 2022 at 17:08)
- ✔ Capture matched object (3 messages, latest: Apr 17 2022 at 12:43)
- Parser Expression Grammars (PVS and Lean comparison) (10 messages, latest: Apr 17 2022 at 00:10)
- ✔ Understanding the
_example
term in the local context (6 messages, latest: Apr 16 2022 at 14:29) - Understanding the
_example
term in the local context (2 messages, latest: Apr 16 2022 at 13:33) - Circumventing "motive not type-correct" (33 messages, latest: Apr 15 2022 at 16:56)
- Converting a simple function from Lean3 to Lean4 (4 messages, latest: Apr 15 2022 at 14:15)
- active patterns (13 messages, latest: Apr 13 2022 at 19:27)
- Print different goals when the cursor is scanning a tactic (17 messages, latest: Apr 13 2022 at 16:29)
- Most idiomatic way to (meta)programatically generate inducti (13 messages, latest: Apr 13 2022 at 15:23)
- constructor and field doc strings (39 messages, latest: Apr 13 2022 at 02:50)
- ✔ unreachable match case (9 messages, latest: Apr 12 2022 at 13:52)
- unreachable match case (4 messages, latest: Apr 12 2022 at 13:18)
- Working with primitive projections (10 messages, latest: Apr 11 2022 at 23:53)
- ✔ Unfolding the type of a variable creates a new variable (3 messages, latest: Apr 11 2022 at 16:07)
- ✔ Not a member of List (3 messages, latest: Apr 11 2022 at 15:52)
- Unfolding the type of a variable creates a new variable (8 messages, latest: Apr 11 2022 at 15:14)
- hygiene frontend bug? (13 messages, latest: Apr 10 2022 at 21:22)
- Not a member of List (4 messages, latest: Apr 10 2022 at 21:05)
- Performance issues with big case split (18 messages, latest: Apr 09 2022 at 21:52)
- FFI for fixed-length arrays (89 messages, latest: Apr 09 2022 at 18:52)
- ✔ Simp extension (2 messages, latest: Apr 09 2022 at 12:20)
- Surprising change in type inference (4 messages, latest: Apr 09 2022 at 03:56)
- type error with Prop? (3 messages, latest: Apr 08 2022 at 21:20)
- Simp extension (12 messages, latest: Apr 08 2022 at 20:41)
- type error? (1 message, latest: Apr 08 2022 at 20:06)
- anonymous structure types (13 messages, latest: Apr 08 2022 at 08:55)
- a "timeit" command (7 messages, latest: Apr 08 2022 at 08:26)
- Issue using a Type 1 in forIn (89 messages, latest: Apr 07 2022 at 19:38)
- Option.get (5 messages, latest: Apr 06 2022 at 17:33)
- ✔ Force-cancelling a task? (1 message, latest: Apr 06 2022 at 07:44)
- Force-cancelling a task? (1 message, latest: Apr 05 2022 at 21:12)
- inductive definition (9 messages, latest: Apr 05 2022 at 19:44)
- ✔ Mutual Recursion (1 message, latest: Apr 05 2022 at 19:20)
- Mutual Recursion (4 messages, latest: Apr 05 2022 at 19:06)
- Coinduction? (20 messages, latest: Apr 05 2022 at 10:56)
- How to get unreflected value of declaration from an attribut (11 messages, latest: Apr 04 2022 at 23:37)
- Properly axiomatizing foreign functions (6 messages, latest: Apr 04 2022 at 22:38)
- Notation for inductive types (4 messages, latest: Apr 04 2022 at 20:37)
- ✔ How to run CommandElabM in an attribute handler? (8 messages, latest: Apr 04 2022 at 20:18)
- How to run CommandElabM in an attribute handler? (14 messages, latest: Apr 04 2022 at 18:35)
- Make some macro-introduced identifiers visible outside (27 messages, latest: Apr 04 2022 at 12:37)
- ✔ Running tactics at the meta level (2 messages, latest: Apr 04 2022 at 04:46)
- Running tactics at the meta level (3 messages, latest: Apr 04 2022 at 04:10)
- termination of syntax consumption (7 messages, latest: Apr 03 2022 at 05:15)
- Tree with fixed branching (14 messages, latest: Apr 02 2022 at 19:35)
- ✔ failed to generate equational theorem (2 messages, latest: Apr 02 2022 at 12:00)
- creating proofs in
TermElabM
(12 messages, latest: Apr 02 2022 at 03:03) - failed to generate equational theorem (15 messages, latest: Apr 01 2022 at 22:51)
- Partial evaluation of a file (99 messages, latest: Apr 01 2022 at 17:36)
- unfold with simp to reduce match (9 messages, latest: Apr 01 2022 at 14:25)
- stack overflow in refine (2 messages, latest: Apr 01 2022 at 01:13)
- SepBy matcher being too greedy? (3 messages, latest: Mar 31 2022 at 20:48)
- ✔ parser expected ')''.html) (5 messages, latest: Mar 31 2022 at 20:01)
- conflicting asterisk for syntax matching (7 messages, latest: Mar 31 2022 at 19:44)
- ✔
decide
and recursion (2 messages, latest: Mar 31 2022 at 17:47) - Semantics of
incQuotDepth
? (4 messages, latest: Mar 31 2022 at 16:13) - Bug in
incQuotDepth
? (1 message, latest: Mar 31 2022 at 11:54) - Nondeterminism during compilation (26 messages, latest: Mar 31 2022 at 07:51)
decide
and recursion (5 messages, latest: Mar 30 2022 at 23:07)- ✔ requiring proofs on inductive constructors (9 messages, latest: Mar 30 2022 at 22:06)
- Reusing inbuilt syntax? (5 messages, latest: Mar 30 2022 at 18:13)
- Syntax -> Name (51 messages, latest: Mar 30 2022 at 16:59)
- ✔ how to revert to lean3 in elan? (2 messages, latest: Mar 30 2022 at 12:54)
- how to revert to lean3 in elan? (2 messages, latest: Mar 30 2022 at 04:21)
- Can I use Lean 4 without Mathlib4? (2 messages, latest: Mar 29 2022 at 18:41)
- ✔ requiring proofs on mutual definitions (15 messages, latest: Mar 29 2022 at 15:49)
- ✔ Where and how to find basic theorems? (2 messages, latest: Mar 29 2022 at 14:54)
- ✔ Repackaging
Nat.add
(1 message, latest: Mar 29 2022 at 01:11) - Repackaging
Nat.add
(3 messages, latest: Mar 28 2022 at 19:23) - ✔ using higher-order functions on inductive types: termin… (5 messages, latest: Mar 27 2022 at 20:06)
- self-hosted M1 mac github actions runner (11 messages, latest: Mar 27 2022 at 16:03)
- Where and how to find basic theorems? (4 messages, latest: Mar 27 2022 at 15:57)
- library_search (4 messages, latest: Mar 27 2022 at 15:32)
- ✔ Lean nested syntax extension with identifiers (4 messages, latest: Mar 27 2022 at 12:37)
- Lean nested syntax extension with identifiers (2 messages, latest: Mar 27 2022 at 12:12)
- Redefining the elaborator for the
simp
attribute (1 message, latest: Mar 27 2022 at 05:08) - Heterogenous operation triggers CoeHTCT (1 message, latest: Mar 25 2022 at 20:56)
- LeanInk/Alectryon (36 messages, latest: Mar 25 2022 at 16:05)
- Proof extraction (1 message, latest: Mar 25 2022 at 13:12)
- ✔ Compiler ICE (1 message, latest: Mar 25 2022 at 07:31)
- Compiler ICE (5 messages, latest: Mar 25 2022 at 01:47)
- Lean 4.0.0-m4 release (3 messages, latest: Mar 24 2022 at 23:53)
- how to document
partial
restriction? (2 messages, latest: Mar 24 2022 at 20:49) - Install using elan missing (2 messages, latest: Mar 24 2022 at 18:27)
- Question about
elabTermEnsuringType
(2 messages, latest: Mar 24 2022 at 17:31) - Repr instance for functions (10 messages, latest: Mar 24 2022 at 16:53)
- Decidable equality (8 messages, latest: Mar 24 2022 at 10:57)
- ✔ Error: unknown free variable '_uniq.402' (1 message, latest: Mar 23 2022 at 21:37)
- ✔ Improving this syntax (1 message, latest: Mar 23 2022 at 21:37)
- Running a lean script with custom library path (1 message, latest: Mar 23 2022 at 18:19)
- ✔
nonDepLet
(3 messages, latest: Mar 23 2022 at 16:06) - Improving this syntax (8 messages, latest: Mar 23 2022 at 14:14)
- ✔ Generating
Expr
terms by quoting (2 messages, latest: Mar 23 2022 at 11:34) - Generating
Expr
terms by quoting (10 messages, latest: Mar 23 2022 at 09:23) - Decidable proposition (11 messages, latest: Mar 23 2022 at 07:20)
- Auto eliminate match (19 messages, latest: Mar 22 2022 at 21:39)
- code generator does not support recursor (68 messages, latest: Mar 22 2022 at 08:25)
repeat
not an identifier? (11 messages, latest: Mar 21 2022 at 22:11)- iterative definition (8 messages, latest: Mar 21 2022 at 18:48)
- fails to reduce? (31 messages, latest: Mar 21 2022 at 17:18)
- ✔ reduction of dependent return type (5 messages, latest: Mar 21 2022 at 14:54)
- reduction of dependent return type (4 messages, latest: Mar 21 2022 at 13:08)
- bundling additive groups and multiplicative groups (4 messages, latest: Mar 20 2022 at 23:31)
- conv and case (6 messages, latest: Mar 20 2022 at 18:37)
- How to use
registerSimpAttr
? (39 messages, latest: Mar 20 2022 at 17:07) - parser category for structure fields? (7 messages, latest: Mar 20 2022 at 12:49)
- using indentation to resolve syntactic ambiguity (5 messages, latest: Mar 20 2022 at 03:34)
- Custom tooltips from macros (9 messages, latest: Mar 19 2022 at 20:03)
- Typeclass instance problem? (17 messages, latest: Mar 19 2022 at 18:51)
- formal semantics (6 messages, latest: Mar 19 2022 at 17:59)
- Reading Inductive definition in Lean4 (7 messages, latest: Mar 19 2022 at 11:29)
- Custom errors from macro-elaborated code? (24 messages, latest: Mar 19 2022 at 06:08)
- ✔ Sigma type (6 messages, latest: Mar 19 2022 at 01:51)
- Lean 4 monads (14 messages, latest: Mar 19 2022 at 01:26)
- Option do notation regression? (55 messages, latest: Mar 19 2022 at 00:29)
- ✔ chaining expressions with arrows (28 messages, latest: Mar 18 2022 at 18:47)
- chaining expressions with arrows (2 messages, latest: Mar 18 2022 at 15:12)
- "default handlers" when deriving DecidableEq (15 messages, latest: Mar 17 2022 at 20:40)
- "Awesome Lean4" page? (22 messages, latest: Mar 17 2022 at 19:52)
- Lint without compiling to .so (5 messages, latest: Mar 17 2022 at 19:21)
- Potential PR to implement ApplyNewGoals in lean4 (4 messages, latest: Mar 16 2022 at 22:31)
- Applying post invariant to Hoare State Monad (4 messages, latest: Mar 16 2022 at 22:29)
- ✔ Prettier Int.le proof (9 messages, latest: Mar 16 2022 at 18:33)
- Error: unknown free variable '_uniq.402' (7 messages, latest: Mar 16 2022 at 17:13)
- ✔ trying to prove false (6 messages, latest: Mar 16 2022 at 16:29)
- trying to prove false (2 messages, latest: Mar 16 2022 at 16:14)
- ✔ Fin without wrapping (3 messages, latest: Mar 16 2022 at 13:11)
- ✔
this
in context (4 messages, latest: Mar 16 2022 at 12:38) this
in context (9 messages, latest: Mar 16 2022 at 09:12)- Fin without wrapping (188 messages, latest: Mar 16 2022 at 06:27)
- ✔ Gadts (3 messages, latest: Mar 16 2022 at 03:51)
- Gadts (24 messages, latest: Mar 15 2022 at 23:56)
- dot notation on bundled homs (5 messages, latest: Mar 15 2022 at 20:45)
- Accessors (11 messages, latest: Mar 14 2022 at 21:27)
- stream events (2 messages, latest: Mar 14 2022 at 20:01)
- using higher-order functions on inductive types: termination (37 messages, latest: Mar 14 2022 at 16:05)
- ✔ Constrain function input to one constructor (2 messages, latest: Mar 14 2022 at 14:29)
- Constrain function input to one constructor (25 messages, latest: Mar 14 2022 at 04:26)
- Forward reasoning in Lean 4: sharing some work (1 message, latest: Mar 14 2022 at 02:36)
- ✔ Inference rules in type class resolution (17 messages, latest: Mar 13 2022 at 18:07)
- Inference rules in type class resolution (4 messages, latest: Mar 13 2022 at 17:06)
- How to get subtype element (4 messages, latest: Mar 12 2022 at 23:35)
- folding definitions (12 messages, latest: Mar 12 2022 at 23:23)
- Subtype vs Set (4 messages, latest: Mar 12 2022 at 19:35)
- ✔ What is PUnit (vs Unit)? (3 messages, latest: Mar 12 2022 at 01:47)
- new lean4-samples repo (8 messages, latest: Mar 12 2022 at 01:13)
- ✔ Unfold fail & LazyList nested induction issue (4 messages, latest: Mar 11 2022 at 22:41)
- Proofs (1 message, latest: Mar 11 2022 at 21:32)
- Unfold fail & LazyList nested induction issue (4 messages, latest: Mar 11 2022 at 20:55)
- hidden benefit? (12 messages, latest: Mar 11 2022 at 20:44)
- ✔ lean4 change tactic change? (3 messages, latest: Mar 11 2022 at 19:23)
- noncomputable theory (4 messages, latest: Mar 11 2022 at 19:22)
- lean4 change tactic change? (7 messages, latest: Mar 11 2022 at 17:36)
- ✔ Trying to understand StateRefT, ST.Ref, STWorld (4 messages, latest: Mar 11 2022 at 15:55)
- Trying to understand StateRefT, ST.Ref, STWorld (3 messages, latest: Mar 11 2022 at 15:09)
- doc-gen4 package name & lakefile parsing (4 messages, latest: Mar 11 2022 at 03:07)
- Inferred namespace syntax (1 message, latest: Mar 11 2022 at 01:07)
- Stuck defining custom syntax (10 messages, latest: Mar 10 2022 at 21:18)
- ✔ 'rewrite' failed but it should work (2 messages, latest: Mar 10 2022 at 19:13)
- 'rewrite' failed but it should work (2 messages, latest: Mar 10 2022 at 18:35)
- do notation + loops (2 messages, latest: Mar 10 2022 at 15:05)
- Unfold fails (2 messages, latest: Mar 10 2022 at 10:13)
- ✔ Understanding
nomatch
(1 message, latest: Mar 10 2022 at 10:11) - fibonacci functions (57 messages, latest: Mar 10 2022 at 02:47)
- doc-gen4 package name (1 message, latest: Mar 09 2022 at 23:09)
- Typeclass outParam vs type member (2 messages, latest: Mar 09 2022 at 20:18)
- io fustration (40 messages, latest: Mar 09 2022 at 18:53)
- ✔ scientificLit (17 messages, latest: Mar 08 2022 at 20:07)
- ✔ Concurrency primitives - augment with proofs? (2 messages, latest: Mar 08 2022 at 18:15)
- Universe inference (6 messages, latest: Mar 08 2022 at 17:27)
- Regression in implicit argument inference (18 messages, latest: Mar 08 2022 at 17:08)
- Lean SQL initiatives (5 messages, latest: Mar 08 2022 at 01:23)
- Concurrency primitives - augment with proofs? (7 messages, latest: Mar 07 2022 at 21:46)
- LeanMySQL feedback (77 messages, latest: Mar 07 2022 at 21:14)
- StdGen (IORef?) Bug (5 messages, latest: Mar 07 2022 at 10:00)
- ✔ Syntax.SepArray bug? (5 messages, latest: Mar 06 2022 at 15:23)
- Syntax.SepArray bug? (2 messages, latest: Mar 06 2022 at 15:04)
- lol another WASM question (11 messages, latest: Mar 06 2022 at 10:12)
decreasing_by
borked? (5 messages, latest: Mar 04 2022 at 23:41)- reordering modulo AC (7 messages, latest: Mar 04 2022 at 21:11)
- ✔ strange type mismatch (7 messages, latest: Mar 04 2022 at 19:07)
- auto for Lean4 (3 messages, latest: Mar 03 2022 at 23:57)
- Nightly broke well-founded proof (11 messages, latest: Mar 02 2022 at 23:28)
- ✔ Possible bug in Lean/Parser/Basic.lean:setExpectedFn (3 messages, latest: Mar 02 2022 at 15:57)
- Possible bug in Lean/Parser/Basic.lean:setExpectedFn (1 message, latest: Mar 02 2022 at 14:58)
- ✔ universal quantification elimination (2 messages, latest: Mar 02 2022 at 13:46)
- Implicit variables from context (7 messages, latest: Mar 02 2022 at 00:02)
- Aesop upddate (4 messages, latest: Mar 01 2022 at 11:51)
- inductive variable bindings (30 messages, latest: Mar 01 2022 at 10:08)
- VSCode "problems" with commands (#) (5 messages, latest: Mar 01 2022 at 08:30)
- universal quantification elimination (4 messages, latest: Mar 01 2022 at 03:16)
- help (14 messages, latest: Mar 01 2022 at 01:16)
- when to declare_syntax_cat (5 messages, latest: Feb 28 2022 at 23:22)
- boost confidence w/o a proof (18 messages, latest: Feb 28 2022 at 20:16)
- computed/cached fields (6 messages, latest: Feb 28 2022 at 15:10)
- docs4# (75 messages, latest: Feb 28 2022 at 10:06)
- local elaborators (17 messages, latest: Feb 27 2022 at 20:42)
- Understanding
nomatch
(7 messages, latest: Feb 27 2022 at 18:05) - ✔ Basic order Lemma (7 messages, latest: Feb 27 2022 at 17:00)
- Retrieve actual path in vscode (4 messages, latest: Feb 27 2022 at 09:34)
- have h : x = x via tactic (2 messages, latest: Feb 27 2022 at 05:02)
- Should this be added to lean 4? (157 messages, latest: Feb 27 2022 at 03:48)
- ✔ Inequalities on Nat literals without tactics? (8 messages, latest: Feb 27 2022 at 00:25)
- OfNat instance not found (15 messages, latest: Feb 26 2022 at 22:36)
- Building lean4_docs like mathlib4_docs (2 messages, latest: Feb 26 2022 at 22:33)
- ✔ Why the angle brakcets? (10 messages, latest: Feb 26 2022 at 22:14)
- quickchecks
Gen
monad (32 messages, latest: Feb 26 2022 at 20:18) - ✔ Syntax questions (1 message, latest: Feb 25 2022 at 22:10)
- ✔ Failed to synthesize instance ToString Term (1 message, latest: Feb 25 2022 at 22:09)
- Visualization of typeclass inference (8 messages, latest: Feb 25 2022 at 19:02)
- M1 Universal Binary (5 messages, latest: Feb 25 2022 at 16:25)
- magical witness (24 messages, latest: Feb 25 2022 at 15:26)
- ✔ unfold loops indefinitely (2 messages, latest: Feb 25 2022 at 09:55)
- Package index for Lean 4 (1 message, latest: Feb 25 2022 at 06:49)
- ✔ What does '@&' mean? (1 message, latest: Feb 24 2022 at 21:32)
- What does '@&' mean? (3 messages, latest: Feb 24 2022 at 20:41)
- Package registry for Lean 4 (6 messages, latest: Feb 24 2022 at 16:34)
- http client (4 messages, latest: Feb 24 2022 at 11:27)
- Trouble with a
rw
(3 messages, latest: Feb 24 2022 at 05:24) - fallible rename_i (8 messages, latest: Feb 23 2022 at 17:00)
- unfold loops indefinitely (5 messages, latest: Feb 23 2022 at 11:30)
- private access (3 messages, latest: Feb 23 2022 at 08:37)
- ✔ better way to write
rangeStepAux
(1 message, latest: Feb 23 2022 at 03:00) - better way to write
rangeStepAux
(115 messages, latest: Feb 23 2022 at 01:17) - how to use
decreasing_by
(11 messages, latest: Feb 23 2022 at 00:45) - ✔ using hygienic 'dagger' names (10 messages, latest: Feb 22 2022 at 18:27)
- IEEE floats (32 messages, latest: Feb 22 2022 at 02:46)
- Simp and structure projection problem (1 message, latest: Feb 21 2022 at 22:00)
- ✔ error handling with result (2 messages, latest: Feb 21 2022 at 17:34)
- tactic 'generalize' failed (5 messages, latest: Feb 21 2022 at 15:57)
- error handling with result (9 messages, latest: Feb 21 2022 at 14:53)
- ✔ Syntax or built-in for negation introduction? (5 messages, latest: Feb 21 2022 at 05:53)
- Syntax or built-in for negation introduction? (3 messages, latest: Feb 21 2022 at 01:49)
- termination_by proof (6 messages, latest: Feb 20 2022 at 16:56)
- CLI library design (23 messages, latest: Feb 20 2022 at 00:25)
- docgen4 not working? (74 messages, latest: Feb 19 2022 at 20:25)
- local instance reduction bug (1 message, latest: Feb 19 2022 at 20:01)
- Compile-time large data (19 messages, latest: Feb 19 2022 at 10:42)
- Failed to synthesize instance ToString Term (5 messages, latest: Feb 19 2022 at 08:45)
- Syntax questions (15 messages, latest: Feb 19 2022 at 00:21)
- ✔ Termination via well founded relation on subtype? (1 message, latest: Feb 18 2022 at 19:30)
- Termination via well founded relation on subtype? (14 messages, latest: Feb 18 2022 at 18:43)
- Strange timing results? (4 messages, latest: Feb 18 2022 at 17:22)
- tactic state in custom command (4 messages, latest: Feb 18 2022 at 10:57)
- implicit arguments (18 messages, latest: Feb 18 2022 at 03:31)
- type argument conversion (8 messages, latest: Feb 18 2022 at 00:22)
- termination IR check failed unexpected type (2 messages, latest: Feb 17 2022 at 18:51)
- assert in lean? (20 messages, latest: Feb 17 2022 at 18:06)
- lsp and emacs (3 messages, latest: Feb 17 2022 at 17:44)
- get default value (6 messages, latest: Feb 17 2022 at 15:53)
- sealing unsafe (14 messages, latest: Feb 17 2022 at 02:24)
- ✔ How to avoid stack overflows? (3 messages, latest: Feb 16 2022 at 18:09)
- ✔ termination by (1 message, latest: Feb 16 2022 at 17:16)
- termination by (66 messages, latest: Feb 16 2022 at 16:50)
- verified compiler (21 messages, latest: Feb 16 2022 at 10:27)
- ✔ match gaurds (1 message, latest: Feb 16 2022 at 01:15)
- match gaurds (7 messages, latest: Feb 15 2022 at 23:08)
- Add position info to module doc (2 messages, latest: Feb 15 2022 at 18:31)
- ✔ docs4# (10 messages, latest: Feb 15 2022 at 05:50)
- running doc-gen4 on lean4 (5 messages, latest: Feb 14 2022 at 19:04)
- Tactics to be ported to mathlib4 (5 messages, latest: Feb 14 2022 at 18:58)
- How to call the declaration elaborator (10 messages, latest: Feb 14 2022 at 16:52)
- ✔ Proving a "not for all" with an "exists" with Classical (6 messages, latest: Feb 14 2022 at 03:25)
- Proving a "not for all" with an "exists" with Classical (5 messages, latest: Feb 14 2022 at 01:04)
- ✔ Is there or-elimination with match? (3 messages, latest: Feb 13 2022 at 22:52)
- Is there or-elimination with match? (8 messages, latest: Feb 13 2022 at 21:39)
- tabled resolution vs e-graphs (1 message, latest: Feb 13 2022 at 14:35)
- ✔ Proving termination in nested inductives (1 message, latest: Feb 13 2022 at 12:26)
- ✔ Mem synthesis fails (1 message, latest: Feb 13 2022 at 11:10)
- WITS'22 talk "Gotta prove fast" (1 message, latest: Feb 13 2022 at 10:42)
- lazy lists (26 messages, latest: Feb 13 2022 at 09:25)
- Mem synthesis fails (15 messages, latest: Feb 13 2022 at 08:51)
- equality substitution (27 messages, latest: Feb 13 2022 at 01:03)
- forallBoundedTelescope (7 messages, latest: Feb 12 2022 at 17:51)
- ✔ Failed to generate equational theorem (2 messages, latest: Feb 12 2022 at 17:49)
- Proving termination in nested inductives (12 messages, latest: Feb 12 2022 at 16:45)
- Failed to generate equational theorem (2 messages, latest: Feb 12 2022 at 15:58)
- error: 'Id' has already been declared (6 messages, latest: Feb 12 2022 at 13:04)
- Proving theorems about functions involving equality rewrites (4 messages, latest: Feb 12 2022 at 12:47)
- Type theory of lean 4 (23 messages, latest: Feb 12 2022 at 02:09)
- Opaque type with interface (18 messages, latest: Feb 11 2022 at 22:59)
- SE question: OOP features in proof assistants (1 message, latest: Feb 11 2022 at 20:43)
- Lake and Lean3 (2 messages, latest: Feb 11 2022 at 20:05)
- Literate programming in Lean4 / Lean4 + Org mode (14 messages, latest: Feb 11 2022 at 15:14)
- Lean 4 basic error (10 messages, latest: Feb 11 2022 at 14:52)
- set_option per project (9 messages, latest: Feb 11 2022 at 14:23)
- [A](topic/A.html) (10 messages, latest: Feb 11 2022 at 11:37)
- auto-bound implicits (6 messages, latest: Feb 11 2022 at 10:08)
- Code folding in language server (2 messages, latest: Feb 10 2022 at 21:01)
- Review on vscode marketplace (3 messages, latest: Feb 10 2022 at 19:48)
- matching expressions (6 messages, latest: Feb 10 2022 at 12:12)
- abbreviations in vscode (31 messages, latest: Feb 10 2022 at 04:09)
- VSCode OK but lake build link error (6 messages, latest: Feb 10 2022 at 04:09)
- failed to synthesize implicit argument (20 messages, latest: Feb 09 2022 at 22:11)
- Tactic writing (10 messages, latest: Feb 09 2022 at 20:12)
- Lean ABI stability (5 messages, latest: Feb 09 2022 at 15:25)
- wasm nix emscripten build (43 messages, latest: Feb 09 2022 at 10:36)
- ✔ GUI LIbs (15 messages, latest: Feb 09 2022 at 10:22)
- ✔ typeclass resolution? (2 messages, latest: Feb 08 2022 at 21:23)
- typeclass resolution? (4 messages, latest: Feb 08 2022 at 21:05)
- (static) multimethods in Lean (2 messages, latest: Feb 08 2022 at 15:42)
- collection of lean4 projects (2 messages, latest: Feb 08 2022 at 14:32)
- language server (8 messages, latest: Feb 08 2022 at 11:02)
- making lean and lean4 coexist (30 messages, latest: Feb 08 2022 at 10:30)
- ✔ IO and Char utilities from the library (1 message, latest: Feb 08 2022 at 07:17)
- IO and Char utilities from the library (3 messages, latest: Feb 08 2022 at 07:05)
- lake seccomp (4 messages, latest: Feb 07 2022 at 17:58)
- New Member (3 messages, latest: Feb 07 2022 at 15:07)
- ✔ Pretty printing equations (3 messages, latest: Feb 07 2022 at 09:55)
- ✔ Obtaining the definition associated with a partial (5 messages, latest: Feb 06 2022 at 16:07)
- Coverage and executed code (13 messages, latest: Feb 06 2022 at 14:45)
- repeat automatically does refl? (17 messages, latest: Feb 06 2022 at 04:27)
- Steps to Install lean4 (with Vscode support) on a new M1 Mac (22 messages, latest: Feb 05 2022 at 19:13)
- VS Code 0.0.6x - Goofin' (19 messages, latest: Feb 05 2022 at 17:13)
- Intellij Plugin? (15 messages, latest: Feb 05 2022 at 16:22)
- Keep VS Code from replacing escape sequence? (11 messages, latest: Feb 05 2022 at 07:16)
- style question (2 messages, latest: Feb 05 2022 at 01:43)
- Pretty printing equations (18 messages, latest: Feb 04 2022 at 21:56)
- Haskell 'Num'-like class hierarchy (2 messages, latest: Feb 04 2022 at 21:07)
- smarter subst? (8 messages, latest: Feb 04 2022 at 16:40)
- ✔ Change lean version in vscode . (15 messages, latest: Feb 04 2022 at 14:53)
- ✔ Setting option in compiled code (3 messages, latest: Feb 04 2022 at 14:50)
- ✔ macro error (2 messages, latest: Feb 04 2022 at 14:46)
- ✔ generic constraints (1 message, latest: Feb 04 2022 at 14:27)
- ✔ Concurrency in TermElabM (2 messages, latest: Feb 04 2022 at 11:14)
- Concurrency in TermElabM (2 messages, latest: Feb 04 2022 at 09:28)
- generic constraints (5 messages, latest: Feb 04 2022 at 02:35)
- ✔ ".0" in expressions (9 messages, latest: Feb 03 2022 at 18:53)
- ✔ Chapters that make no sense (2 messages, latest: Feb 03 2022 at 13:57)
- Infix functions (5 messages, latest: Feb 03 2022 at 12:03)
- Pattern match actions (13 messages, latest: Feb 03 2022 at 10:40)
- ✔ Parsing error when adding a comment (11 messages, latest: Feb 03 2022 at 00:36)
- Additive/multiplicative split in Lean 4 (19 messages, latest: Feb 02 2022 at 22:00)
do
dsl (32 messages, latest: Feb 02 2022 at 21:22)- ✔ VS Code 0.0.60 - Manual refresh necessary (16 messages, latest: Feb 02 2022 at 15:08)
- Need suggestions to improve a DSL for dimensional calculus (30 messages, latest: Feb 02 2022 at 05:44)
- smalltt (and Lean) benchmarks (1 message, latest: Feb 01 2022 at 12:30)
- Chapters that make no sense (8 messages, latest: Feb 01 2022 at 12:18)
- ✔ Partial application with typeclass instance (3 messages, latest: Feb 01 2022 at 01:41)
- VS Code 0.0.60 - Manual refresh necessary (6 messages, latest: Jan 31 2022 at 20:03)
- ✔ Conflict between definitional and propositional equality (12 messages, latest: Jan 31 2022 at 15:34)
- ✔ inductive datatype parameter mismatch (4 messages, latest: Jan 31 2022 at 13:01)
- inductive datatype parameter mismatch (4 messages, latest: Jan 31 2022 at 11:07)
- BTree feedback (1 message, latest: Jan 31 2022 at 04:16)
- ✔ binaries with autocompletion (6 messages, latest: Jan 29 2022 at 14:46)
- Making Lean 4 compiler more functional and monolith (11 messages, latest: Jan 29 2022 at 13:27)
- Discrepancy between TC synthesis in Lean 3 and 4 (3 messages, latest: Jan 29 2022 at 11:26)
- binaries with autocompletion (3 messages, latest: Jan 28 2022 at 23:06)
- Gotta prove fast (8 messages, latest: Jan 28 2022 at 15:11)
- Understanding outParam (3 messages, latest: Jan 27 2022 at 19:53)
- ✔ Reducible definition and TC problem (1 message, latest: Jan 26 2022 at 21:26)
- trying to understand termination (33 messages, latest: Jan 26 2022 at 21:00)
- Reducible definition and TC problem (16 messages, latest: Jan 26 2022 at 19:56)
- Termination works in Lean 3, but fails in Lean 4 (12 messages, latest: Jan 26 2022 at 15:14)
- ✔ documentation (2 messages, latest: Jan 26 2022 at 08:02)
- View patterns (5 messages, latest: Jan 25 2022 at 19:16)
- No goal to be solved error (13 messages, latest: Jan 25 2022 at 00:20)
- mathlib / lean3 / lean4 status? (4 messages, latest: Jan 24 2022 at 23:30)
- documentation (27 messages, latest: Jan 24 2022 at 21:09)
- Summing intermediate list slower than summing directly? (6 messages, latest: Jan 24 2022 at 20:05)
- for, unexpected need for type ascription (92 messages, latest: Jan 24 2022 at 19:30)
- structural recursion cannot be used (6 messages, latest: Jan 24 2022 at 06:25)
- elaboration function has not been implemented (8 messages, latest: Jan 23 2022 at 20:52)
- Help tracking down a Lean bug (3 messages, latest: Jan 22 2022 at 17:53)
- Prevent rebuilding package dependency (7 messages, latest: Jan 22 2022 at 13:05)
- Monad with LocalContext in State (3 messages, latest: Jan 22 2022 at 11:16)
- ✔ Wasm? (6 messages, latest: Jan 21 2022 at 17:04)
- type checker in lean4 (6 messages, latest: Jan 21 2022 at 15:24)
- GUI LIbs (2 messages, latest: Jan 21 2022 at 04:50)
- timeout at 'whnf' in forallTelescope (5 messages, latest: Jan 20 2022 at 15:23)
- C FFI for enums and structs (22 messages, latest: Jan 20 2022 at 14:35)
- Package manager (6 messages, latest: Jan 19 2022 at 17:50)
- leanproject (24 messages, latest: Jan 19 2022 at 17:31)
- ✔ List.enumerate (15 messages, latest: Jan 19 2022 at 15:43)
- Name binding in macro? (3 messages, latest: Jan 19 2022 at 08:19)
- List.enumerate (7 messages, latest: Jan 19 2022 at 01:51)
- Lake mathport panic (3 messages, latest: Jan 19 2022 at 00:57)
- Building shared library with lake (35 messages, latest: Jan 18 2022 at 12:40)
- Specialized sorry for Type and Prop (11 messages, latest: Jan 18 2022 at 00:45)
- ✔ Will Lean 4 always be “Lean 4” (1 message, latest: Jan 17 2022 at 23:50)
- REPL (13 messages, latest: Jan 17 2022 at 22:19)
- Will Lean 4 always be “Lean 4” (1 message, latest: Jan 17 2022 at 21:30)
- Will Lean4 always be “Lean4” (3 messages, latest: Jan 17 2022 at 21:07)
- Derive handlers (32 messages, latest: Jan 17 2022 at 16:59)
- How do I print out the "normal form" of a Lean4 program? (6 messages, latest: Jan 17 2022 at 15:27)
- multiple packages in one repo with Lake (3 messages, latest: Jan 17 2022 at 02:05)
- ✔ mkSimpAttr (53 messages, latest: Jan 16 2022 at 21:23)
- ✔ Obtaining imports of a specific module (7 messages, latest: Jan 16 2022 at 13:42)
- ✔ freeing pointers in FFI (1 message, latest: Jan 16 2022 at 10:49)
- lake scripts with args (5 messages, latest: Jan 15 2022 at 19:27)
- Obtaining imports of a specific module (8 messages, latest: Jan 15 2022 at 17:15)
- PointedType (5 messages, latest: Jan 15 2022 at 16:09)
- freeing pointers in FFI (114 messages, latest: Jan 15 2022 at 02:50)
- ✔ Help compiling simple finally tagless DSL (1 message, latest: Jan 14 2022 at 16:31)
- Help compiling simple finally tagless DSL (3 messages, latest: Jan 14 2022 at 15:57)
- parsing text with lean (6 messages, latest: Jan 14 2022 at 12:16)
- Help compiling simple finally tagless DSL (cross-posted) (1 message, latest: Jan 14 2022 at 01:31)
- ackermann (9 messages, latest: Jan 13 2022 at 18:22)
- Termination of bubble sort (6 messages, latest: Jan 13 2022 at 17:59)
- easy HashMap instantiation (13 messages, latest: Jan 13 2022 at 15:21)
- ✔ @[simp] not working? (3 messages, latest: Jan 12 2022 at 16:35)
- ✔ induction deconstruction on hypotheses (3 messages, latest: Jan 12 2022 at 16:16)
- @[simp] not working? (21 messages, latest: Jan 12 2022 at 15:33)
- induction deconstruction on hypotheses (11 messages, latest: Jan 12 2022 at 14:46)
- unknown package 'CLI' in emacs (11 messages, latest: Jan 11 2022 at 17:52)
- match in quasiquotation (25 messages, latest: Jan 11 2022 at 17:11)
- ✔ Derived Ord instance (2 messages, latest: Jan 11 2022 at 10:38)
- ✔ syntax objects for structure update expressions (2 messages, latest: Jan 10 2022 at 15:17)
- no need to close namespace (5 messages, latest: Jan 10 2022 at 10:00)
- syntax objects for structure update expressions (5 messages, latest: Jan 10 2022 at 07:45)
- Obtain git revision of the compiler (4 messages, latest: Jan 09 2022 at 21:48)
- debugging maximum recursion depth (4 messages, latest: Jan 09 2022 at 12:51)
- ✔ Syntax for maps (1 message, latest: Jan 08 2022 at 13:59)
- Syntax for maps (2 messages, latest: Jan 08 2022 at 10:45)
- doc-gen4 preview (1 message, latest: Jan 07 2022 at 10:01)
- ✔ Lake Main.lean file (5 messages, latest: Jan 07 2022 at 07:23)
- The Syntax of the Import Section (19 messages, latest: Jan 06 2022 at 23:01)
- Lean Manual (1 message, latest: Jan 06 2022 at 02:58)
- Adding Lake itself as a dependency? (5 messages, latest: Jan 06 2022 at 01:59)
- termination_by (27 messages, latest: Jan 05 2022 at 17:56)
- Debugging Exprs (6 messages, latest: Jan 05 2022 at 13:38)
- group theory: mathlib4 (3 messages, latest: Jan 04 2022 at 14:36)
- CPDT in lean (16 messages, latest: Jan 04 2022 at 03:37)
- Contents of lean4 nix shell (2 messages, latest: Jan 03 2022 at 22:52)
- Treating
Float
as reals, inconsistent? (46 messages, latest: Jan 03 2022 at 22:04) - ✔ help with two proofs (7 messages, latest: Jan 03 2022 at 21:23)
- help with two proofs (11 messages, latest: Jan 03 2022 at 21:09)
- ✔ debugging simp (5 messages, latest: Jan 03 2022 at 17:00)
- Shallow clones (1 message, latest: Jan 02 2022 at 15:09)
- Conv pattern and typeclasses problem (1 message, latest: Jan 02 2022 at 10:42)
- Slow sort then dedup (18 messages, latest: Dec 31 2021 at 02:46)
- formalizing music theory (10 messages, latest: Dec 30 2021 at 23:45)
- ✔ Spawned >1000 tasks. Have 4 cores. Program only uses 2. (25 messages, latest: Dec 30 2021 at 17:40)
- Understanding partial (2 messages, latest: Dec 30 2021 at 17:08)
- Use proof in custom tactic (14 messages, latest: Dec 30 2021 at 13:38)
- newtype (10 messages, latest: Dec 29 2021 at 00:06)
- ✔ Lake not present (6 messages, latest: Dec 28 2021 at 23:04)
- Invalid parser (8 messages, latest: Dec 28 2021 at 17:09)
- Syntax from object (4 messages, latest: Dec 28 2021 at 13:04)
- mkSimpAttr (20 messages, latest: Dec 27 2021 at 19:06)
- [PSA] don't modify the environment in ParametricAttribute (1 message, latest: Dec 27 2021 at 16:13)
- What comes after macros? (11 messages, latest: Dec 27 2021 at 16:10)
- Derived Ord instance (1 message, latest: Dec 27 2021 at 03:55)
- adding library dependencies to compiler (8 messages, latest: Dec 26 2021 at 13:57)
- ✔ CoqSearch and friends? (1 message, latest: Dec 25 2021 at 19:41)
- ✔ Disable prelude? (2 messages, latest: Dec 25 2021 at 19:38)
- CoqSearch and friends? (6 messages, latest: Dec 25 2021 at 16:23)
- Disable prelude? (2 messages, latest: Dec 25 2021 at 15:45)
- ✔ UTF-8 bug (4 messages, latest: Dec 25 2021 at 12:46)
- Function application delaboration (35 messages, latest: Dec 23 2021 at 22:01)
- Attribute casing convention (12 messages, latest: Dec 23 2021 at 15:23)
- As Task Join (3 messages, latest: Dec 23 2021 at 10:58)
- Inductive Bug with Array + Prop (47 messages, latest: Dec 23 2021 at 08:16)
- ✔ Using foreign functions with –plugin (1 message, latest: Dec 22 2021 at 21:35)
- Using foreign functions with –plugin (6 messages, latest: Dec 22 2021 at 17:31)
- ✔ populated HashMap (14 messages, latest: Dec 22 2021 at 17:07)
- ✔ Self hosted kernel (1 message, latest: Dec 22 2021 at 10:06)
- Self hosted kernel (6 messages, latest: Dec 22 2021 at 08:53)
- ✔ return type of a function (13 messages, latest: Dec 22 2021 at 02:45)
- html in doc-gen4 (51 messages, latest: Dec 21 2021 at 10:44)
- ✔ Order of running, Tasks in Main (21 messages, latest: Dec 21 2021 at 10:39)
- Order of running, Tasks in Main (2 messages, latest: Dec 21 2021 at 08:00)
- Debug traces for non-terminating tactic (5 messages, latest: Dec 20 2021 at 20:05)
OfNat 1
vshas_one
(3 messages, latest: Dec 20 2021 at 14:10)- ✔ accessing MetaM from IO (2 messages, latest: Dec 20 2021 at 02:10)
- Isn't Fin a bad type for safe array lookup? (35 messages, latest: Dec 20 2021 at 00:59)
- accessing MetaM from IO (4 messages, latest: Dec 20 2021 at 00:57)
- Typeclass timeout and outParam (30 messages, latest: Dec 20 2021 at 00:26)
- Option.get! (7 messages, latest: Dec 19 2021 at 14:47)
- ✔ Typeclass timeout and outParam (1 message, latest: Dec 19 2021 at 11:06)
- advent of code!!! (86 messages, latest: Dec 19 2021 at 10:57)
- Hypothesis in
match
(5 messages, latest: Dec 19 2021 at 10:56) - simp type error (2 messages, latest: Dec 18 2021 at 14:51)
- examining well-founded def (8 messages, latest: Dec 17 2021 at 22:59)
- ✔ Confused by the order of the implicit argument insertion (1 message, latest: Dec 17 2021 at 13:55)
- ✔ How are attributes defined? (1 message, latest: Dec 17 2021 at 00:40)
- How are attributes defined? (5 messages, latest: Dec 16 2021 at 23:11)
- ✔ Is Prod associative? (7 messages, latest: Dec 16 2021 at 20:48)
- Confused by the order of the implicit argument insertion (9 messages, latest: Dec 16 2021 at 20:14)
- Is Prod associative? (1 message, latest: Dec 16 2021 at 18:57)
- User defined option (5 messages, latest: Dec 16 2021 at 17:10)
- simp failing with "application type mismatch Eq.ndrec …" (8 messages, latest: Dec 16 2021 at 01:45)
- termination compiler app error (10 messages, latest: Dec 16 2021 at 00:19)
- ✔ Lake update (?) broke VSCode integration (1 message, latest: Dec 15 2021 at 22:01)
- match proof irrelevance (4 messages, latest: Dec 15 2021 at 21:46)
- Single rewrite with simp (9 messages, latest: Dec 15 2021 at 18:09)
- ✔ Has the do notation changed recently? (166 messages, latest: Dec 14 2021 at 23:31)
- Generating documentation? (6 messages, latest: Dec 14 2021 at 20:10)
- find all lean files recursively (1 message, latest: Dec 14 2021 at 18:12)
- include lean.h (28 messages, latest: Dec 14 2021 at 16:11)
- Lake update (?) broke VSCode integration (3 messages, latest: Dec 14 2021 at 09:35)
- mwe: plugin? (23 messages, latest: Dec 13 2021 at 19:04)
- Arithmetic solver (19 messages, latest: Dec 13 2021 at 18:38)
- Custom attribute that also adds
extern
(3 messages, latest: Dec 13 2021 at 03:48) - c code generation at compile time (50 messages, latest: Dec 13 2021 at 00:53)
- ✔ Odd type class failure (7 messages, latest: Dec 12 2021 at 21:05)
- Odd type class failure (8 messages, latest: Dec 12 2021 at 20:11)
- vscode (11 messages, latest: Dec 12 2021 at 13:28)
- ✔ non valid occurrence of datatype with trees (4 messages, latest: Dec 11 2021 at 19:58)
- ✔ include_str! or similar (12 messages, latest: Dec 11 2021 at 16:58)
- nightly 12.11.2021 not published for Linux (2 messages, latest: Dec 11 2021 at 16:27)
- Tactic basics (7 messages, latest: Dec 10 2021 at 23:00)
- c++ code generation at compile time (4 messages, latest: Dec 10 2021 at 19:09)
- leanc doesn't find standard c headers (1 message, latest: Dec 10 2021 at 18:38)
- include_str! or similar (1 message, latest: Dec 10 2021 at 18:27)
- leanpkg++ idea [RFC] (110 messages, latest: Dec 10 2021 at 17:30)
- Class inductive non positive occurence (3 messages, latest: Dec 10 2021 at 17:09)
- ✔ How to create a type generic structure with tuples? (1 message, latest: Dec 10 2021 at 13:00)
- ✔ Lean 4 version of eval_expr (5 messages, latest: Dec 10 2021 at 10:37)
- Lean 4 version of eval_expr (16 messages, latest: Dec 10 2021 at 09:42)
- How to create a type generic structure with tuples? (8 messages, latest: Dec 09 2021 at 21:28)
- pattern matching wrapped in Option (1 message, latest: Dec 09 2021 at 14:41)
- ✔ Check that expression does not typcheck (4 messages, latest: Dec 09 2021 at 12:46)
- Lean4 Debugger (31 messages, latest: Dec 09 2021 at 03:51)
- Cranelift and LLVM (2 messages, latest: Dec 09 2021 at 03:43)
- List of instances (10 messages, latest: Dec 08 2021 at 23:13)
- VSCode extension hanging? (3 messages, latest: Dec 08 2021 at 05:54)
- ✔ Idiomatic nestes for loops (3 messages, latest: Dec 07 2021 at 10:36)
- ✔ Priority for inner product notation (4 messages, latest: Dec 06 2021 at 21:08)
- Priority for inner product notation (2 messages, latest: Dec 06 2021 at 19:59)
- efmt in doc-gen4 (13 messages, latest: Dec 06 2021 at 10:20)
- ✔ Position of a Declaration (2 messages, latest: Dec 05 2021 at 15:49)
- Idiomatic nestes for loops (7 messages, latest: Dec 05 2021 at 12:40)
- failed to synth Applicative Option instance in nightly (6 messages, latest: Dec 04 2021 at 15:24)
- Interface for containers (52 messages, latest: Dec 04 2021 at 11:10)
- Position of a Declaration (1 message, latest: Dec 03 2021 at 21:52)
- tactic termination checking doesn't work for indexed types (1 message, latest: Dec 03 2021 at 20:53)
- termination checking for deep pattern matches (1 message, latest: Dec 03 2021 at 18:05)
- Application type mismatch (5 messages, latest: Dec 03 2021 at 17:59)
- package versioning and dependency pinning (26 messages, latest: Dec 03 2021 at 09:33)
- rfl won't work with indexed inductive types (11 messages, latest: Dec 02 2021 at 00:49)
- Self-contained native toolchain (27 messages, latest: Dec 01 2021 at 11:12)
- [nixos psa] upgrade your elan (1 message, latest: Dec 01 2021 at 10:40)
- Name -> Syntax (2 messages, latest: Dec 01 2021 at 08:23)
- Restricting structure instantiation (26 messages, latest: Dec 01 2021 at 00:34)
- Extern code depending on function argument (21 messages, latest: Nov 30 2021 at 11:04)
- struggling with recursion (33 messages, latest: Nov 29 2021 at 19:52)
- need a little help : p ∨ false ↔ p (41 messages, latest: Nov 29 2021 at 19:42)
- ✔ unintended instance (20 messages, latest: Nov 29 2021 at 09:25)
- editors for Lean 4 (8 messages, latest: Nov 29 2021 at 04:04)
- lean 4 hackers (33 messages, latest: Nov 29 2021 at 00:51)
- unintended instance (1 message, latest: Nov 29 2021 at 00:37)
- query API (26 messages, latest: Nov 28 2021 at 23:54)
- Optionally bracketed binder (5 messages, latest: Nov 28 2021 at 17:38)
- ✔ Unknown introduced variables (2 messages, latest: Nov 28 2021 at 16:20)
- Interface for multi-dimensional arrays (42 messages, latest: Nov 28 2021 at 15:22)
- Misunderstanding default arguments (5 messages, latest: Nov 28 2021 at 10:00)
- Unknown introduced variables (2 messages, latest: Nov 28 2021 at 09:44)
- Strange error (15 messages, latest: Nov 28 2021 at 01:15)
- ✔ emacs lean4-mode (1 message, latest: Nov 27 2021 at 14:12)
- emacs lean4-mode (8 messages, latest: Nov 27 2021 at 14:04)
- ✔ Patterns for auto generated declarations (2 messages, latest: Nov 27 2021 at 12:18)
- Patterns for auto generated declarations (3 messages, latest: Nov 27 2021 at 11:22)
- A nice revelation about meta code (14 messages, latest: Nov 26 2021 at 19:21)
- ✔ boolean eval and equality (3 messages, latest: Nov 26 2021 at 15:50)
- boolean eval and equality (5 messages, latest: Nov 26 2021 at 15:05)
- ✔ constant vs def (4 messages, latest: Nov 25 2021 at 12:05)
- Absolute value for Float (73 messages, latest: Nov 25 2021 at 10:55)
- Cannot find default value for field (15 messages, latest: Nov 25 2021 at 10:19)
- ✔ polytype lists (7 messages, latest: Nov 25 2021 at 03:20)
- polytype lists (1 message, latest: Nov 24 2021 at 21:53)
- Associate value with goal (4 messages, latest: Nov 24 2021 at 16:57)
- ✔ Split And repeatedly (3 messages, latest: Nov 24 2021 at 16:39)
- ✔ Leanc failing to link properly (1 message, latest: Nov 24 2021 at 14:57)
- Double TC extends (7 messages, latest: Nov 24 2021 at 13:52)
- Leanc failing to link properly (8 messages, latest: Nov 23 2021 at 20:56)
- abstraction for tables (10 messages, latest: Nov 23 2021 at 19:24)
- New simp feature (6 messages, latest: Nov 23 2021 at 19:01)
- [undefined reference to _gmpz](topic/undefined.20reference.20to.20__gmpz_.html) (11 messages, latest: Nov 23 2021 at 10:17)
- porting attributes (8 messages, latest: Nov 23 2021 at 08:43)
- Modified typeclass resolution (12 messages, latest: Nov 22 2021 at 23:34)
- Proofs with opaque Bool functions (11 messages, latest: Nov 22 2021 at 14:41)
- Reversed simp priority (7 messages, latest: Nov 22 2021 at 12:45)
- ✔ pipelining as first class citizens? (3 messages, latest: Nov 22 2021 at 09:46)
- Class "inheritance" (8 messages, latest: Nov 22 2021 at 09:37)
- pipelining as first class citizens? (3 messages, latest: Nov 22 2021 at 04:10)
- ✔ moreLeancArgs (7 messages, latest: Nov 21 2021 at 13:58)
- general-purpose programming (15 messages, latest: Nov 20 2021 at 18:24)
- ✔ unknown package 'Ffi' (8 messages, latest: Nov 20 2021 at 15:03)
- Unfold where (2 messages, latest: Nov 20 2021 at 14:51)
- List.filter with Bool (2 messages, latest: Nov 19 2021 at 16:36)
- ✔ Lean server (55 messages, latest: Nov 19 2021 at 14:45)
- ✔ Exfalso HEq (7 messages, latest: Nov 19 2021 at 12:00)
- Name structure constructor (4 messages, latest: Nov 18 2021 at 22:05)
- Exfalso HEq (12 messages, latest: Nov 18 2021 at 20:55)
- Codegen parameter names (2 messages, latest: Nov 18 2021 at 06:06)
- C++17 (30 messages, latest: Nov 17 2021 at 21:25)
- ✔ Lake + Emacs (6 messages, latest: Nov 17 2021 at 18:46)
- Jump to definition across files, in lean4 repo (19 messages, latest: Nov 16 2021 at 09:24)
- simpLocation (8 messages, latest: Nov 15 2021 at 23:38)
- weird class error (49 messages, latest: Nov 15 2021 at 23:14)
- Priority for simp theorems (7 messages, latest: Nov 15 2021 at 21:20)
- Searching in the codebase? (4 messages, latest: Nov 15 2021 at 21:14)
- Herbrand's Unification Theorem (2 messages, latest: Nov 13 2021 at 12:33)
- simplifying typeclass definitions (5 messages, latest: Nov 12 2021 at 21:58)
- Override hypothesis (6 messages, latest: Nov 12 2021 at 15:08)
- Trouble with simp - failed to assign instance (36 messages, latest: Nov 12 2021 at 09:46)
- ✔ append idents in macro (8 messages, latest: Nov 11 2021 at 21:36)
- working with the lean4 repository in VSCode (5 messages, latest: Nov 11 2021 at 09:20)
- lake problem, perhaps macos specific? (22 messages, latest: Nov 11 2021 at 07:01)
- elab_rules (4 messages, latest: Nov 11 2021 at 01:47)
- squeeze_simp (2 messages, latest: Nov 10 2021 at 22:13)
- Error message for non-existent file (10 messages, latest: Nov 10 2021 at 08:26)
- simp type annotations (1 message, latest: Nov 09 2021 at 23:17)
- mathport tests (35 messages, latest: Nov 09 2021 at 15:15)
- ✔ HEq (2 messages, latest: Nov 09 2021 at 10:42)
- Notation unfolding in infoview (2 messages, latest: Nov 09 2021 at 08:58)
- HEq (8 messages, latest: Nov 08 2021 at 14:29)
- Simp does not unify with subexpresion (13 messages, latest: Nov 08 2021 at 09:10)
- C's int type in FFI? (13 messages, latest: Nov 07 2021 at 18:20)
- Structural recursion (36 messages, latest: Nov 07 2021 at 16:30)
- Stack overflow when enumerating a matrix (25 messages, latest: Nov 06 2021 at 16:03)
- Induction not applied to hypothesis (4 messages, latest: Nov 05 2021 at 18:33)
- DecidableRel for Option.lt issue (2 messages, latest: Nov 05 2021 at 04:44)
- optimized re-compilations (15 messages, latest: Nov 04 2021 at 20:59)
- Cases not resolving match (4 messages, latest: Nov 03 2021 at 08:35)
- Explanation for recursor? (2 messages, latest: Nov 02 2021 at 21:17)
- Hiearchy builder in Lean (8 messages, latest: Nov 02 2021 at 16:57)
- ✔ Meta helper for filling universe meta-variables? (2 messages, latest: Nov 01 2021 at 09:13)
- Binding the syntax being matched in
elab_rules
? (3 messages, latest: Nov 01 2021 at 07:21) - Meta helper for filling universe meta-variables? (1 message, latest: Nov 01 2021 at 06:34)
- Breaking instance resolution loop (44 messages, latest: Oct 30 2021 at 19:31)
- Functions with class arguments (2 messages, latest: Oct 28 2021 at 09:29)
- Change in pattern matching; expected behaviour? (6 messages, latest: Oct 27 2021 at 17:33)
- lake linkArgs (15 messages, latest: Oct 25 2021 at 23:03)
- Where does hq come from in this proof? (12 messages, latest: Oct 25 2021 at 19:25)
- No support for code generation (4 messages, latest: Oct 25 2021 at 18:42)
- Cannot send message to unknown document (10 messages, latest: Oct 25 2021 at 16:14)
- IO Tasks (9 messages, latest: Oct 25 2021 at 08:45)
- new stackoverflow question (6 messages, latest: Oct 23 2021 at 19:25)
- Casing convention (9 messages, latest: Oct 23 2021 at 16:18)
- Pattern matching lambda body in conv (28 messages, latest: Oct 22 2021 at 23:33)
- Compare lists by relation (3 messages, latest: Oct 22 2021 at 14:37)
- inferType in delaborator (8 messages, latest: Oct 22 2021 at 10:14)
- ✔ "rerun on save" option for interpreter? (100 messages, latest: Oct 22 2021 at 00:31)
- Variable width C types (15 messages, latest: Oct 21 2021 at 21:02)
- why does leanbin have mathport as a dependency? (49 messages, latest: Oct 21 2021 at 07:06)
- ✔ MData and unification (4 messages, latest: Oct 20 2021 at 23:43)
- Notation for Option? (1 message, latest: Oct 20 2021 at 22:47)
- ✔ Namespacing Issue (5 messages, latest: Oct 20 2021 at 20:09)
- Lean server (19 messages, latest: Oct 20 2021 at 17:05)
- Lake: add to LEAN_PATH via Lake (16 messages, latest: Oct 20 2021 at 04:38)
- ✔ witness for match (19 messages, latest: Oct 20 2021 at 01:41)
- [RFC] Line Comment Change (27 messages, latest: Oct 19 2021 at 16:46)
- ✔ unused let disappears (3 messages, latest: Oct 19 2021 at 08:13)
- "rerun on save" option for interpreter? (1 message, latest: Oct 19 2021 at 05:24)
- No Hashable instance for ByteArray? (9 messages, latest: Oct 19 2021 at 00:26)
- Command terminator (4 messages, latest: Oct 19 2021 at 00:20)
- ✔ Trace while compilation vs goal view (1 message, latest: Oct 18 2021 at 22:19)
- ✔ Simp bug - produces
application type mismatch
(1 message, latest: Oct 18 2021 at 22:19) - Simp bug - produces
application type mismatch
(7 messages, latest: Oct 18 2021 at 21:01) - abbrev vs reducible (2 messages, latest: Oct 18 2021 at 18:56)
- MData and unification (2 messages, latest: Oct 18 2021 at 14:45)
- Expandable trace API (18 messages, latest: Oct 18 2021 at 12:57)
- ✔ Weird deriving error message (10 messages, latest: Oct 18 2021 at 08:11)
- Lake now comes with Lean (13 messages, latest: Oct 17 2021 at 04:50)
- FFI + impure invariants (3 messages, latest: Oct 17 2021 at 04:10)
- Trace while compilation vs goal view (10 messages, latest: Oct 17 2021 at 02:08)
- lake build on Windows - C FFI - undefined reference (6 messages, latest: Oct 16 2021 at 15:06)
- Float.floor (49 messages, latest: Oct 16 2021 at 11:40)
- Dependent Type Ref Counting (10 messages, latest: Oct 15 2021 at 19:29)
- Running bench on CI? (2 messages, latest: Oct 15 2021 at 11:24)
- local bench: feedback? (3 messages, latest: Oct 15 2021 at 09:44)
- What does
repeat
mean? (11 messages, latest: Oct 14 2021 at 21:15) - ✔ create newlines in Syntax (1 message, latest: Oct 14 2021 at 15:23)
- create newlines in Syntax (5 messages, latest: Oct 14 2021 at 13:05)
- dependent array output size (39 messages, latest: Oct 14 2021 at 12:23)
- ✔
inversion
tactic? (8 messages, latest: Oct 14 2021 at 09:02) alias
in Lean 4 (3 messages, latest: Oct 14 2021 at 02:57)- elan now expects lake? (13 messages, latest: Oct 13 2021 at 09:04)
- ✔ Partial def versus def (1 message, latest: Oct 12 2021 at 02:28)
- Partial def versus def (2 messages, latest: Oct 11 2021 at 17:44)
- Aarch64 support (1 message, latest: Oct 11 2021 at 15:25)
- Incorrect escaping of \r ? (4 messages, latest: Oct 11 2021 at 13:18)
- ✔ Pattern matching on Syntax nodes (1 message, latest: Oct 11 2021 at 12:42)
- ✔ qualified imports? (1 message, latest: Oct 11 2021 at 12:42)
- qualified imports? (6 messages, latest: Oct 11 2021 at 09:41)
- Pattern matching on Syntax nodes (5 messages, latest: Oct 10 2021 at 21:59)
- Disabling Macro Hygine? (4 messages, latest: Oct 10 2021 at 07:30)
- ✔ Scoping for delaborator? (10 messages, latest: Oct 09 2021 at 20:35)
- ✔ Using the Delaborator (1 message, latest: Oct 09 2021 at 15:45)
- building on macos (37 messages, latest: Oct 09 2021 at 15:16)
- Scoping for delaborator? (1 message, latest: Oct 09 2021 at 15:03)
- Using the Delaborator (2 messages, latest: Oct 09 2021 at 06:54)
- VSCode Lean4 extension doesn't like
lakefile.lean
(74 messages, latest: Oct 08 2021 at 22:20) - Unexpected macro rule firing? (7 messages, latest: Oct 08 2021 at 17:51)
- ✔ Working with mutable monad (1 message, latest: Oct 08 2021 at 09:01)
- Working with constants (74 messages, latest: Oct 08 2021 at 08:56)
- Working with mutable monad (8 messages, latest: Oct 07 2021 at 10:04)
- package repository? (2 messages, latest: Oct 07 2021 at 08:46)
- Tips for writing conversion tactic (4 messages, latest: Oct 07 2021 at 08:22)
- ✔ Lean4 interpreter hanging for map to iterated products (1 message, latest: Oct 07 2021 at 03:17)
- Lean4 interpreter hanging for map to iterated products (4 messages, latest: Oct 07 2021 at 00:34)
- Option coercion (5 messages, latest: Oct 06 2021 at 23:16)
- pp.beta (6 messages, latest: Oct 06 2021 at 20:56)
- ✔ Argument for tactic as expression (2 messages, latest: Oct 06 2021 at 09:26)
- Argument for tactic as expression (1 message, latest: Oct 06 2021 at 08:55)
- Weird initialize error (2 messages, latest: Oct 05 2021 at 14:23)
- Normalization in a macro? (4 messages, latest: Oct 05 2021 at 07:20)
- ✔ Implicit type arg v. forall (2 messages, latest: Oct 04 2021 at 22:43)
- PANIC at Lean.Expr.bindingDomain! Lean.Expr:618:23: binding (2 messages, latest: Oct 04 2021 at 20:25)
- ✔ Monad return with $ (8 messages, latest: Oct 04 2021 at 20:00)
- ✔ Problems when writing a socket package (32 messages, latest: Oct 04 2021 at 17:29)
- ✔ Universes (4 messages, latest: Oct 04 2021 at 17:16)
- ✔ Updating local context in tactics (2 messages, latest: Oct 04 2021 at 08:48)
- ✔ 3 or 4? (1 message, latest: Oct 04 2021 at 08:34)
- Tactic state filtering (12 messages, latest: Oct 04 2021 at 07:37)
- ✔ character prefix to int in macro (1 message, latest: Oct 04 2021 at 07:13)
- 3 or 4? (2 messages, latest: Oct 03 2021 at 18:45)
- build requirements for Lean4 (2 messages, latest: Oct 03 2021 at 02:21)
- Export format (29 messages, latest: Oct 02 2021 at 22:12)
- New attribute to mark theorems (9 messages, latest: Oct 02 2021 at 16:42)
- Rewrite tactic fails in lambda body (5 messages, latest: Oct 02 2021 at 16:22)
- ✔ using MacroM effectively (3 messages, latest: Oct 02 2021 at 16:14)
- character prefix to int in macro (6 messages, latest: Oct 02 2021 at 16:12)
- ✔ What does congrArg stand for? (9 messages, latest: Oct 02 2021 at 11:58)
- ✔ Where clause in inductive (2 messages, latest: Oct 01 2021 at 19:25)
- Definitional equality with patterns (5 messages, latest: Oct 01 2021 at 11:47)
- [test-mathport] errors (7 messages, latest: Oct 01 2021 at 11:10)
- Updating local context in tactics (3 messages, latest: Oct 01 2021 at 09:30)
- Required type annotation using Array (6 messages, latest: Oct 01 2021 at 05:29)
- ✔ space separated sepBy? (1 message, latest: Oct 01 2021 at 04:53)
- space separated sepBy? (3 messages, latest: Oct 01 2021 at 04:06)
- Processing sepBy's (1 message, latest: Oct 01 2021 at 03:11)
- ✔ Macros without prefix/suffix (2 messages, latest: Oct 01 2021 at 02:40)
- Macros without prefix/suffix (3 messages, latest: Oct 01 2021 at 01:58)
- ✔ partial+mutual crash again (4 messages, latest: Sep 30 2021 at 19:58)
- ✔ implementedBy + mutual (4 messages, latest: Sep 30 2021 at 19:26)
- partial+mutual crash again (2 messages, latest: Sep 30 2021 at 19:06)
- ✔ Macros: parse dyck grammar? (1 message, latest: Sep 30 2021 at 17:23)
- ✔ macro v/s typeclass resolution (1 message, latest: Sep 30 2021 at 17:23)
- implementedBy + mutual (3 messages, latest: Sep 30 2021 at 17:10)
- Where clause in inductive (6 messages, latest: Sep 30 2021 at 16:40)
- ✔ What is a bracket anyway? (1 message, latest: Sep 30 2021 at 16:12)
- What is a bracket anyway? (15 messages, latest: Sep 30 2021 at 13:28)
- [RFC] name/version package fields (602 messages, latest: Sep 30 2021 at 10:49)
- ✔ Typing the Placeholder char (1 message, latest: Sep 30 2021 at 03:51)
- ✔ programming and termination (7 messages, latest: Sep 30 2021 at 02:30)
- macro v/s typeclass resolution (7 messages, latest: Sep 29 2021 at 23:45)
- Macros: parse dyck grammar? (11 messages, latest: Sep 29 2021 at 22:44)
- Handling potentially infinite loop? (21 messages, latest: Sep 29 2021 at 16:53)
- #find (12 messages, latest: Sep 29 2021 at 07:27)
- Segfault due to mutual recursion? (126 messages, latest: Sep 29 2021 at 06:25)
- Simplifications in proofs/type-checking not happening; wh… (7 messages, latest: Sep 29 2021 at 00:44)
- What is leanc and how to use it (1 message, latest: Sep 29 2021 at 00:14)
- Typing the Placeholder char (12 messages, latest: Sep 28 2021 at 22:27)
- Using
timeit
for the entire program (4 messages, latest: Sep 28 2021 at 20:44) - Problems when writing a socket package (4 messages, latest: Sep 28 2021 at 15:17)
- detecting presence of main function without full elaboration (3 messages, latest: Sep 28 2021 at 12:42)
- Forced to disambiguate when using instance method (16 messages, latest: Sep 28 2021 at 09:47)
- simp is not picking up a theorem (13 messages, latest: Sep 27 2021 at 16:30)
- Asking for simplifications in proofs/type-checking (6 messages, latest: Sep 26 2021 at 14:06)
- ✔ Type refinement in dependent pattern matching (2 messages, latest: Sep 25 2021 at 18:43)
- Notation precedence (3 messages, latest: Sep 25 2021 at 16:47)
- ✔ panic on match equality proof (4 messages, latest: Sep 24 2021 at 20:56)
- panic on match equality proof (2 messages, latest: Sep 24 2021 at 17:49)
- Dealing with f (h ▸ b) (7 messages, latest: Sep 24 2021 at 14:57)
- Questions on Fin type and def/abbrev (20 messages, latest: Sep 24 2021 at 10:48)
- lake (24 messages, latest: Sep 24 2021 at 01:42)
- Tactic by manipulating Expr (9 messages, latest: Sep 23 2021 at 21:41)
- Type refinement in dependent pattern matching (4 messages, latest: Sep 23 2021 at 21:35)
- ✔ Proving equality from arrow equality (90 messages, latest: Sep 23 2021 at 11:35)
- a tiny ninja build generator (1 message, latest: Sep 22 2021 at 20:59)
- Attempting to define An interval (14 messages, latest: Sep 21 2021 at 23:41)
- induction on mutual inductives fails (16 messages, latest: Sep 21 2021 at 19:17)
- String to Float (11 messages, latest: Sep 21 2021 at 15:56)
- non-structured, non-anonymous cases (9 messages, latest: Sep 21 2021 at 08:27)
- Shared libraries (5 messages, latest: Sep 20 2021 at 15:42)
- ✔ Type annotation prevents elaboration of universe level (7 messages, latest: Sep 20 2021 at 15:18)
- Type annotation prevents elaboration of universe level (1 message, latest: Sep 20 2021 at 11:25)
- manyIndent (5 messages, latest: Sep 20 2021 at 11:20)
- ✔ Unification and meta-variables in mkAppM' (2 messages, latest: Sep 18 2021 at 15:24)
- Unification and meta-variables in mkAppM' (3 messages, latest: Sep 18 2021 at 14:29)
- Fast inline compiler for numerical computing (94 messages, latest: Sep 18 2021 at 00:50)
- ✔ Running lean function from c++ (1 message, latest: Sep 17 2021 at 21:45)
- ✔ Arithmetic Progression With Lean (8 messages, latest: Sep 17 2021 at 18:21)
- Arithmetic Progression With Lean (2 messages, latest: Sep 17 2021 at 18:12)
- Running lean function from c++ (7 messages, latest: Sep 17 2021 at 16:47)
- ✔ generalise appbuilder (8 messages, latest: Sep 16 2021 at 19:07)
- tactic naming convention (13 messages, latest: Sep 16 2021 at 18:39)
- trace classes (3 messages, latest: Sep 16 2021 at 14:03)
- Unicode symbols (37 messages, latest: Sep 16 2021 at 07:26)
- The Lean C/C++ API (38 messages, latest: Sep 15 2021 at 13:49)
- generalise appbuilder (1 message, latest: Sep 15 2021 at 09:39)
- Stuck at solving universe constraint (10 messages, latest: Sep 14 2021 at 16:38)
MonadLiftT Id
instance (5 messages, latest: Sep 14 2021 at 15:16)- Alternative ways to use Lean4 outside of VSCode? (4 messages, latest: Sep 13 2021 at 19:28)
- Preventing Parser Backtracking (10 messages, latest: Sep 13 2021 at 19:15)
- renameI can't handle composite names (2 messages, latest: Sep 13 2021 at 13:45)
- ✔ Rewrite issue (10 messages, latest: Sep 13 2021 at 02:42)
- Lean 4 macro paper "binding position" (13 messages, latest: Sep 13 2021 at 01:25)
- Rewrite issue (5 messages, latest: Sep 12 2021 at 16:36)
- Trouble understanding the theorem process (18 messages, latest: Sep 12 2021 at 07:35)
- INTERNAL PANIC: out of memory (10 messages, latest: Sep 12 2021 at 07:07)
- segfault in mkParserOfConstantUnsafe (4 messages, latest: Sep 11 2021 at 22:26)
- ✔ LINK_OPTS rdynamic + path? (2 messages, latest: Sep 11 2021 at 17:22)
- strange stack overflow when parsing(?) tactics (21 messages, latest: Sep 10 2021 at 15:37)
- ✔ Eq.ndrec vs Eq.rec (1 message, latest: Sep 10 2021 at 10:15)
- Eq.ndrec vs Eq.rec (2 messages, latest: Sep 09 2021 at 21:36)
- ✔ Elaboration performance large inductive types (4 messages, latest: Sep 08 2021 at 20:36)
- ✔ Inductively-defined propositions (11 messages, latest: Sep 08 2021 at 13:17)
- Java AST in Lean4 (58 messages, latest: Sep 08 2021 at 12:59)
- ✔ Using result from foreign function in a tactic (2 messages, latest: Sep 06 2021 at 14:41)
- Elaboration performance large inductive types (12 messages, latest: Sep 06 2021 at 09:31)
- ✔ Building let expressions (8 messages, latest: Sep 06 2021 at 09:26)
- Building let expressions (3 messages, latest: Sep 06 2021 at 09:03)
- Developing locally on Mac with Conda (6 messages, latest: Sep 05 2021 at 19:35)
- ✔ Weird Type Mismatch Error (4 messages, latest: Sep 05 2021 at 16:51)
- ✔ implementation of tactic mode? (1 message, latest: Sep 05 2021 at 02:47)
- Round trip elaboration (1 message, latest: Sep 05 2021 at 02:32)
- Weird Type Mismatch Error (1 message, latest: Sep 05 2021 at 01:42)
- implementation of tactic mode? (3 messages, latest: Sep 05 2021 at 01:29)
- Using result from foreign function in a tactic (3 messages, latest: Sep 03 2021 at 10:28)
- ✔ invalid pattern variable (17 messages, latest: Sep 03 2021 at 03:30)
- Dave's Garage Benchmark (10 messages, latest: Sep 02 2021 at 15:53)
- ✔ Naive question: safety of tactics (2 messages, latest: Sep 01 2021 at 12:23)
- Naive question: safety of tactics (8 messages, latest: Sep 01 2021 at 12:17)
- ✔ Syntax highlightling (1 message, latest: Aug 31 2021 at 09:18)
- Syntax highlightling (8 messages, latest: Aug 31 2021 at 09:03)
- Variable command bug? (2 messages, latest: Aug 30 2021 at 16:06)
- ✔ Type Mismatch? (1 message, latest: Aug 30 2021 at 14:25)
- Type Mismatch? (8 messages, latest: Aug 30 2021 at 12:19)
- ✔ Specifying the motive(s) using the
induction
tactic (1 message, latest: Aug 30 2021 at 05:11) - ✔ Wellfounded recursion (1 message, latest: Aug 30 2021 at 05:10)
- Wellfounded recursion (5 messages, latest: Aug 29 2021 at 23:41)
- Specifying the motive(s) using the
induction
tactic (3 messages, latest: Aug 29 2021 at 18:41) - why no universe inference in theorems? (3 messages, latest: Aug 29 2021 at 14:11)
- Lean server
-D
settings (3 messages, latest: Aug 29 2021 at 08:39) - ✔ Is lean4 ripe enough for my Ph.D. dissertation? (5 messages, latest: Aug 29 2021 at 07:55)
- An LLVM IR metaprogram (9 messages, latest: Aug 29 2021 at 01:54)
- merging goals tactic (8 messages, latest: Aug 28 2021 at 18:21)
- ✔ simp match question (3 messages, latest: Aug 27 2021 at 19:07)
- Mysterious array access performance (93 messages, latest: Aug 27 2021 at 18:16)
- simp match question (1 message, latest: Aug 27 2021 at 15:11)
- (0: ℕ).succ workaround? (12 messages, latest: Aug 27 2021 at 03:06)
- ✔ induction with fixed index (2 messages, latest: Aug 26 2021 at 21:37)
- induction with fixed index (3 messages, latest: Aug 26 2021 at 21:02)
- ✔ Induction alternative name when using Quot.ind? (2 messages, latest: Aug 26 2021 at 18:18)
- Induction alternative name when using Quot.ind? (3 messages, latest: Aug 26 2021 at 18:12)
- leanmake choosing nix store over elan (5 messages, latest: Aug 25 2021 at 00:47)
- Handling
ite
s (4 messages, latest: Aug 24 2021 at 11:21) - elan update (7 messages, latest: Aug 24 2021 at 01:04)
- instance not synthesizing issue? (3 messages, latest: Aug 24 2021 at 00:48)
- Ending a command (4 messages, latest: Aug 23 2021 at 17:44)
- fin pattern matching less smart? (2 messages, latest: Aug 23 2021 at 12:50)
- unexpanders (18 messages, latest: Aug 23 2021 at 00:07)
- Server crashes on
extern
(31 messages, latest: Aug 21 2021 at 07:54) - Should
universe u v
generate an error? (5 messages, latest: Aug 20 2021 at 19:48) - Instantiating MVars in decls (3 messages, latest: Aug 20 2021 at 17:20)
- parenthesize error: unknown constant 'null' (40 messages, latest: Aug 20 2021 at 16:07)
- Ensuring tail recursion (2 messages, latest: Aug 20 2021 at 08:38)
- Running
extern
declarations (6 messages, latest: Aug 19 2021 at 22:27) - inferInstance (11 messages, latest: Aug 19 2021 at 17:23)
- Structure diamond error (2 messages, latest: Aug 19 2021 at 14:50)
- Another IO Task question (135 messages, latest: Aug 19 2021 at 09:07)
syntax
that doesn't wrap the node? (31 messages, latest: Aug 18 2021 at 22:59)- Simulating well founded recursions? (22 messages, latest: Aug 18 2021 at 12:38)
- Odd precedence in syntax command (2 messages, latest: Aug 18 2021 at 11:52)
- Mutual inductive rec (17 messages, latest: Aug 18 2021 at 08:17)
- Elaboration time of `example : (List.range 500).length = 500 (16 messages, latest: Aug 18 2021 at 03:02)
- panic while testing ring tactic (2 messages, latest: Aug 18 2021 at 02:38)
- "pure
do
block" error misnomer? (17 messages, latest: Aug 17 2021 at 20:41) - How to WHNF without exposing recursors? (5 messages, latest: Aug 17 2021 at 19:33)
- Problems when updating Lean (21 messages, latest: Aug 17 2021 at 14:44)
- ✔ Mutual inductive rec (6 messages, latest: Aug 17 2021 at 10:22)
- benchmarking commands (8 messages, latest: Aug 17 2021 at 05:54)
- ✔ Environment extensions in importModules (1 message, latest: Aug 17 2021 at 02:39)
- Environment extensions in importModules (3 messages, latest: Aug 17 2021 at 01:05)
- ✔ Use recursor within inductive def (1 message, latest: Aug 16 2021 at 13:16)
- Tactic for changing hypothesis (2 messages, latest: Aug 15 2021 at 13:28)
- extends and namespaces (3 messages, latest: Aug 15 2021 at 13:26)
- Stale branches (4 messages, latest: Aug 14 2021 at 16:29)
- ✔ has_reflect (8 messages, latest: Aug 13 2021 at 19:43)
- has_reflect (4 messages, latest: Aug 13 2021 at 15:02)
- ✔ mk_instance (2 messages, latest: Aug 13 2021 at 13:29)
- mk_instance (1 message, latest: Aug 13 2021 at 12:52)
- How to add user attributes? (5 messages, latest: Aug 10 2021 at 19:18)
- Reflection in Lean4 (4 messages, latest: Aug 10 2021 at 15:36)
- typeclass failure (35 messages, latest: Aug 10 2021 at 10:13)
- Use recursor within inductive def (38 messages, latest: Aug 10 2021 at 09:44)
- Fun with macros (16 messages, latest: Aug 08 2021 at 19:22)
- ✔ VS Code Issue (4 messages, latest: Aug 08 2021 at 16:40)
- hang/segfault on import (23 messages, latest: Aug 08 2021 at 14:47)
- macro nonReservedSymbol? (4 messages, latest: Aug 08 2021 at 12:32)
nonReservedSymbol
in macros? (1 message, latest: Aug 08 2021 at 06:02)- Defining notation (2 messages, latest: Aug 08 2021 at 05:04)
- Writing Tactics (20 messages, latest: Aug 08 2021 at 04:47)
- Compile package as plugin (17 messages, latest: Aug 07 2021 at 00:45)
- ✔ IO Tasks (1 message, latest: Aug 07 2021 at 00:41)
- performance regression in nightly-2021-08-04? (11 messages, latest: Aug 05 2021 at 03:36)
- ✔ Understanding notation (5 messages, latest: Aug 03 2021 at 16:42)
- Rw makes 2 goals (1 message, latest: Aug 03 2021 at 13:07)
- Rewrite one side of eq (2 messages, latest: Aug 03 2021 at 12:43)
- Trouble resolving extern code (6 messages, latest: Aug 02 2021 at 19:08)
- Style for using external code (9 messages, latest: Aug 02 2021 at 15:35)
- ✔
apply_instance
for Decidable propositions (12 messages, latest: Aug 01 2021 at 18:55) - subtypes and
(a : α)
(16 messages, latest: Jul 31 2021 at 19:35) apply_instance
for Decidable propositions (15 messages, latest: Jul 29 2021 at 19:18)- IO.FS.removeAll (6 messages, latest: Jul 29 2021 at 12:05)
- Cross-version olean imports (1 message, latest: Jul 28 2021 at 20:17)
- Literal Map syntax? (4 messages, latest: Jul 28 2021 at 13:04)
- user attributes (24 messages, latest: Jul 28 2021 at 12:47)
- fun+match with implicit (3 messages, latest: Jul 26 2021 at 21:15)
- ✔ Proving Nat less than is well-founded (2 messages, latest: Jul 25 2021 at 19:49)
- ✔ Required Project Structure? (2 messages, latest: Jul 24 2021 at 08:50)
- Required Project Structure? (3 messages, latest: Jul 24 2021 at 07:56)
- universe options (3 messages, latest: Jul 24 2021 at 07:38)
- Using syntax with quotations (4 messages, latest: Jul 23 2021 at 03:44)
- ✔ Lean 4 on M1 Mac (14 messages, latest: Jul 22 2021 at 10:42)
- Breaking up large mutual inductives (50 messages, latest: Jul 22 2021 at 09:35)
- backporting Nat.Le (1 message, latest: Jul 22 2021 at 00:49)
- Proving Nat less than is well-founded (5 messages, latest: Jul 21 2021 at 19:48)
- reducing inductive result types (12 messages, latest: Jul 21 2021 at 16:13)
- ✔ ctrl-/ "toggle comment" broken in vscode-lean4 0.0.32 (2 messages, latest: Jul 17 2021 at 04:48)
- Strange stack overflow / timeout (41 messages, latest: Jul 17 2021 at 02:11)
- ctrl-/ "toggle comment" broken in vscode-lean4 0.0.32 (3 messages, latest: Jul 16 2021 at 21:06)
- let overload (57 messages, latest: Jul 16 2021 at 17:35)
- How to use hand written parsers (41 messages, latest: Jul 14 2021 at 08:57)
- Pretty printing library (1 message, latest: Jul 14 2021 at 06:53)
- module doc comments (1 message, latest: Jul 14 2021 at 03:46)
- expected "prelude", got "prelude" (18 messages, latest: Jul 14 2021 at 02:03)
- position dependent macros (6 messages, latest: Jul 14 2021 at 01:50)
- SeqRight
HAndThen
(5 messages, latest: Jul 14 2021 at 00:20) - <- lifting through do quotation (1 message, latest: Jul 13 2021 at 00:28)
- Syntax quotation for &"ident" parsers (10 messages, latest: Jul 12 2021 at 21:02)
- Punit docstring typo? (4 messages, latest: Jul 12 2021 at 20:19)
- Rewriting specific term (1 message, latest: Jul 11 2021 at 15:02)
- Not true by definition (10 messages, latest: Jul 11 2021 at 07:37)
- Many1 antiquotations (5 messages, latest: Jul 10 2021 at 08:29)
- implicit vs explicit (2 messages, latest: Jul 10 2021 at 08:04)
- Tuple vs. Anon Ctor (6 messages, latest: Jul 10 2021 at 01:00)
- lean –run unknown package (4 messages, latest: Jul 09 2021 at 19:34)
- simp and nat lits (4 messages, latest: Jul 08 2021 at 18:05)
- Querying category parsers (34 messages, latest: Jul 08 2021 at 14:49)
extern
constants in server mode (6 messages, latest: Jul 07 2021 at 05:11)- Deriving curiosty (2 messages, latest: Jul 06 2021 at 23:12)
- Quoting commands (20 messages, latest: Jul 06 2021 at 21:30)
- Generics and containers in Lean (4 messages, latest: Jul 06 2021 at 21:16)
- Renaming in root? (3 messages, latest: Jul 06 2021 at 20:32)
- (deleted) (1 message, latest: Jul 06 2021 at 17:46)
- Unary/prefix minus precedence bug? (12 messages, latest: Jul 06 2021 at 04:01)
- UInt* structure codegen (5 messages, latest: Jul 05 2021 at 21:28)
- Unsafe inhabited constants (4 messages, latest: Jul 05 2021 at 18:52)
- programmatically (ab)use lean4 (3 messages, latest: Jul 04 2021 at 08:36)
- playing with lean4 (15 messages, latest: Jul 04 2021 at 02:09)
- heterogenous operators and coercions (7 messages, latest: Jul 03 2021 at 15:48)
- Function.Equiv (5 messages, latest: Jul 02 2021 at 17:44)
- FromJson exponential blowup (1 message, latest: Jul 02 2021 at 00:52)
- Lean 4 set_like (22 messages, latest: Jul 01 2021 at 23:26)
- Matching a conditional in a theorem (7 messages, latest: Jul 01 2021 at 02:17)
- Alternate Int Hierarchy (23 messages, latest: Jun 29 2021 at 21:50)
- builtin_initialize leads to "unknown declaration 'initFn…' (15 messages, latest: Jun 29 2021 at 11:47)
- Lean 4 SAT Solver-Prover (4 messages, latest: Jun 28 2021 at 10:27)
- vscode-Infoview: goals accomplished but not (4 messages, latest: Jun 28 2021 at 03:29)
- lean4 plans (6 messages, latest: Jun 26 2021 at 20:07)
- bound quantifier experiments (16 messages, latest: Jun 24 2021 at 22:04)
- [rfc] kill the child workers (15 messages, latest: Jun 23 2021 at 18:24)
- Server error in inductives (9 messages, latest: Jun 23 2021 at 16:56)
- Matching on Exprs (3 messages, latest: Jun 23 2021 at 11:37)
- Serialisation to oleans (3 messages, latest: Jun 22 2021 at 14:17)
- [rfc] make trace[…] lazy (2 messages, latest: Jun 22 2021 at 11:22)
- Misunderstanding of simp (30 messages, latest: Jun 22 2021 at 04:15)
- Incorrect Name Mangling (2 messages, latest: Jun 21 2021 at 18:09)
- Preventing attribute syntax from stealing identifiers (7 messages, latest: Jun 21 2021 at 13:34)
- lean4-mode: "Error processing message: wrong type argument" (12 messages, latest: Jun 21 2021 at 13:26)
- hasLooseBVar misunderstanding? (4 messages, latest: Jun 20 2021 at 18:23)
- pEmpty (10 messages, latest: Jun 18 2021 at 07:58)
- variable {C} (13 messages, latest: Jun 18 2021 at 01:33)
- Making a RungeKutta 4 (98 messages, latest: Jun 18 2021 at 01:20)
- VS Code Extension LSP stack overflow (4 messages, latest: Jun 16 2021 at 15:40)
- Monad
Of
classes (18 messages, latest: Jun 14 2021 at 13:39) - Reusing knowledge from a pattern match (19 messages, latest: Jun 13 2021 at 19:11)
- Macros in inductives? (8 messages, latest: Jun 12 2021 at 11:40)
- List.append error on cases (4 messages, latest: Jun 11 2021 at 19:15)
- Custom attributes and initialize (12 messages, latest: Jun 11 2021 at 10:17)
- rewrite failure (7 messages, latest: Jun 11 2021 at 08:06)
- Expected Lean 4 build time? (68 messages, latest: Jun 10 2021 at 22:34)
- goal view (82 messages, latest: Jun 10 2021 at 20:20)
- Integrating with reference counting in C++ (9 messages, latest: Jun 09 2021 at 18:21)
- Package with native (foreign) dependencies (6 messages, latest: Jun 09 2021 at 15:53)
- Nested unfolding (10 messages, latest: Jun 09 2021 at 06:41)
- controlling delaboration (22 messages, latest: Jun 08 2021 at 17:27)
- Progress notification server protocol extension p. (Pre-RFC) (8 messages, latest: Jun 07 2021 at 19:13)
- Reading a text file (8 messages, latest: Jun 07 2021 at 18:47)
- Bypass lean functions with lean functions at runtime? (3 messages, latest: Jun 07 2021 at 17:33)
- Don't pattern match on composed constructors? (3 messages, latest: Jun 07 2021 at 13:04)
- Unexpected leanpkg build behavior (4 messages, latest: Jun 07 2021 at 02:06)
- Pi token? (5 messages, latest: Jun 06 2021 at 08:09)
- apf function/tactic? (6 messages, latest: Jun 06 2021 at 07:28)
- Print all typeclasses (1 message, latest: Jun 05 2021 at 16:04)
- 'Running' lean 4 programmes (4 messages, latest: Jun 05 2021 at 14:11)
- Cases on a Bool (4 messages, latest: Jun 05 2021 at 01:59)
- Beta reduction in proofs (4 messages, latest: Jun 04 2021 at 13:11)
- typeclass inference failing with decidable pred (5 messages, latest: Jun 04 2021 at 11:27)
- rfc: theorem names (176 messages, latest: Jun 04 2021 at 10:00)
- [RFC] Try/Else Syntax (24 messages, latest: Jun 04 2021 at 08:48)
- ST.Ref type unsafety (4 messages, latest: Jun 03 2021 at 19:05)
- Trouble with basic pattern matching? (7 messages, latest: Jun 03 2021 at 18:55)
- class diamond: field has already been declared (2 messages, latest: Jun 03 2021 at 14:52)
- Defining mutable rose trees (6 messages, latest: Jun 03 2021 at 12:13)
- hello world tactic (8 messages, latest: Jun 02 2021 at 23:53)
- Lazy evaluation in Option.orElse? (7 messages, latest: Jun 01 2021 at 08:35)
- Need to set elan override for Lean toolchain directories (6 messages, latest: May 31 2021 at 21:13)
- How to read a private definition (10 messages, latest: May 31 2021 at 20:56)
- Partitioning mathlib (181 messages, latest: May 31 2021 at 20:32)
- New LT instance (159 messages, latest: May 31 2021 at 13:01)
- maze game (13 messages, latest: May 31 2021 at 08:41)
- proving boolean equality (4 messages, latest: May 30 2021 at 15:51)
- Error in VSCode (4 messages, latest: May 30 2021 at 11:49)
- list unit (39 messages, latest: May 30 2021 at 03:21)
- leanpkg
path
setting (5 messages, latest: May 29 2021 at 21:23) - Term goal and local context query request s.p.e.p. (Pre-RFC) (2 messages, latest: May 28 2021 at 17:15)
- coercion to function needs some hints (18 messages, latest: May 28 2021 at 14:43)
- invalid field notation (2 messages, latest: May 27 2021 at 19:39)
- An formalized micro-compiler for Krivine machines (1 message, latest: May 26 2021 at 22:15)
- Has Lean 4 gotten slower? (27 messages, latest: May 26 2021 at 22:07)
- Cannot map over lists with more than 8737 elements (3 messages, latest: May 26 2021 at 14:59)
- Simp not simplifying (37 messages, latest: May 26 2021 at 14:11)
- Weird elan error on
elan self update
(8 messages, latest: May 26 2021 at 07:45) - Building plugins on Windows? (2 messages, latest: May 25 2021 at 21:18)
- Synthetic metavariables in exact (15 messages, latest: May 25 2021 at 17:39)
- Lean Hide Root Names/Macros (23 messages, latest: May 25 2021 at 17:07)
- KeyedDeclsAttribute (11 messages, latest: May 25 2021 at 06:19)
- groups (50 messages, latest: May 24 2021 at 19:37)
- negating games (12 messages, latest: May 23 2021 at 11:15)
- Shorter abbreviation for · (11 messages, latest: May 21 2021 at 17:50)
- using nix (96 messages, latest: May 21 2021 at 13:47)
- A package for a more flexible
numLit
(6 messages, latest: May 21 2021 at 09:12) - Mathlib 4 source files (58 messages, latest: May 21 2021 at 00:38)
- Metaprogramming: Importing modules (8 messages, latest: May 20 2021 at 12:20)
- Prevent execution of
#eval
during editing (6 messages, latest: May 19 2021 at 19:39) quote
/toExpr
id/non-id solution [RFC] (48 messages, latest: May 19 2021 at 08:45)- PSA:
Expr.abstract
does not do what you think it does (8 messages, latest: May 19 2021 at 08:39) - PSA:
Expr.abstract
is unsafe (4 messages, latest: May 19 2021 at 08:13) - Yet another expression quotation package (60 messages, latest: May 18 2021 at 19:08)
- Existential quantifier set mem (18 messages, latest: May 18 2021 at 18:35)
- ParserDescr vs. Parser (1 message, latest: May 18 2021 at 00:02)
- Matching Tokens in Macro Patterns (28 messages, latest: May 17 2021 at 20:28)
- Option Flatten? (3 messages, latest: May 17 2021 at 19:12)
- induction on quotients (1 message, latest: May 17 2021 at 08:47)
- theorem (4 messages, latest: May 16 2021 at 18:40)
- Lemmas for functions (16 messages, latest: May 16 2021 at 13:04)
- Field Exports (12 messages, latest: May 16 2021 at 10:40)
- Missing Unexpanders for Core Functions? (18 messages, latest: May 16 2021 at 10:35)
- Run Tests (12 messages, latest: May 16 2021 at 09:54)
- Infix Delaborator Bug? (3 messages, latest: May 15 2021 at 17:37)
- Notation not continuing to override (10 messages, latest: May 15 2021 at 09:44)
- About Tokens (and the Token Cache) (35 messages, latest: May 15 2021 at 02:14)
- structure fields which are functions are better with
where
(4 messages, latest: May 14 2021 at 19:53) - Stop server in VSCode? (10 messages, latest: May 14 2021 at 15:59)
- Local notations : issue and workaround (7 messages, latest: May 14 2021 at 00:17)
- Dependent Syntax (45 messages, latest: May 13 2021 at 23:47)
- class is Type not Prop (9 messages, latest: May 13 2021 at 23:33)
- (x : A . t) implicit argument synthesized by tactic (4 messages, latest: May 13 2021 at 18:41)
- Making sense of the output from #print (3 messages, latest: May 13 2021 at 01:26)
- Mathlib 4 (215 messages, latest: May 11 2021 at 22:46)
- Configuring Time (7 messages, latest: May 11 2021 at 21:54)
- why allow multiple instances per data type? (43 messages, latest: May 11 2021 at 21:27)
- The largest universe (10 messages, latest: May 11 2021 at 20:14)
- Deprecation warnings? (39 messages, latest: May 11 2021 at 20:03)
- unification bug? (4 messages, latest: May 11 2021 at 15:47)
- Unexpected behavior of simp (11 messages, latest: May 11 2021 at 03:10)
- Adventures in tacticSeqs (1 message, latest: May 10 2021 at 22:56)
- Declaring new syntax for greater universes (7 messages, latest: May 10 2021 at 17:13)
- Lean 4 installation issues (24 messages, latest: May 09 2021 at 21:37)
- deep match behind an Option a structure (11 messages, latest: May 09 2021 at 18:08)
- csimp can violate linear access of data (8 messages, latest: May 08 2021 at 13:46)
- Metamath verifier in Lean 4 (19 messages, latest: May 08 2021 at 02:47)
- nice way to define mutually inductive types (13 messages, latest: May 07 2021 at 17:58)
- match don't rewrite context (4 messages, latest: May 07 2021 at 12:51)
- Reference counting instructions for cases (4 messages, latest: May 07 2021 at 11:56)
- Empty string refl (5 messages, latest: May 06 2021 at 17:52)
- Set/Change Command Syntax Category? (3 messages, latest: May 06 2021 at 09:03)
- Lean 4 Info View (2 messages, latest: May 06 2021 at 07:09)
- Creating a DSL (8 messages, latest: May 05 2021 at 20:45)
- Kinds of goals closed by rw/simp only/simp (73 messages, latest: May 05 2021 at 17:40)
- simp behaviour (9 messages, latest: May 05 2021 at 11:25)
- not_or_not in TBA course (10 messages, latest: May 05 2021 at 10:58)
- subscript uparrow (8 messages, latest: May 05 2021 at 06:34)
- Idiomatic Lean for "Do Nothing" (3 messages, latest: May 04 2021 at 04:16)
- Binder bug: Binder not being properly preserved? (12 messages, latest: May 04 2021 at 03:09)
- MetaM and tactics (39 messages, latest: May 03 2021 at 01:23)
- associativity of
↔
(486 messages, latest: May 02 2021 at 21:02) - implementing `(x) (56 messages, latest: May 02 2021 at 21:01)
- (no topic) (1 message, latest: May 02 2021 at 21:00)
- Lean 4 under the hood (77 messages, latest: May 02 2021 at 10:32)
- lean-mode docs/confusion (5 messages, latest: May 01 2021 at 09:10)
- injectivity of inductive constructors (2 messages, latest: Apr 30 2021 at 15:23)
- mathport:wf-refl (14 messages, latest: Apr 30 2021 at 12:50)
- change in
simp
behaviour (25 messages, latest: Apr 30 2021 at 11:23) - State of Lean 3's mathlib tactics (1 message, latest: Apr 30 2021 at 10:28)
- analogue of #print notation (13 messages, latest: Apr 30 2021 at 09:50)
fact
trick (5 messages, latest: Apr 30 2021 at 08:27)- DecidableEq on Ordering (4 messages, latest: Apr 29 2021 at 22:15)
- Unfolding into ite? (5 messages, latest: Apr 29 2021 at 15:06)
- Defining my own numerals (17 messages, latest: Apr 29 2021 at 12:08)
- Default Notation Scope Confusion (34 messages, latest: Apr 28 2021 at 16:55)
- No function coercion on apply? (3 messages, latest: Apr 28 2021 at 15:00)
- OptionM and DecEq (117 messages, latest: Apr 27 2021 at 20:34)
- vscode lean-mode for non-standard project structure? (3 messages, latest: Apr 27 2021 at 17:20)
- Run lean to type check a file (6 messages, latest: Apr 27 2021 at 16:34)
- error position (2 messages, latest: Apr 27 2021 at 09:19)
- structured concurrency (24 messages, latest: Apr 26 2021 at 20:29)
- [emacs] switching between lean-mode and lean4-mode (1 message, latest: Apr 26 2021 at 18:36)
- server hang using tasks (2 messages, latest: Apr 26 2021 at 10:35)
- Instances of Non-classes? (5 messages, latest: Apr 25 2021 at 23:38)
- lean4-mode emacs issues (7 messages, latest: Apr 25 2021 at 17:11)
- Weird Error with Custom Nat Lits (30 messages, latest: Apr 25 2021 at 14:09)
- Are panics Lean bugs? (3 messages, latest: Apr 25 2021 at 06:28)
- to_additive (49 messages, latest: Apr 25 2021 at 02:53)
- Bool MulComm sanity check (9 messages, latest: Apr 24 2021 at 20:45)
- Inspect Tail Recursion (22 messages, latest: Apr 23 2021 at 19:17)
- appUnexpander pitfall (3 messages, latest: Apr 23 2021 at 17:53)
- Error with Digits in Custom Syntax (13 messages, latest: Apr 23 2021 at 07:15)
- Thunk Bind (60 messages, latest: Apr 22 2021 at 14:23)
- Strange behaviour of abbreviations feature with new VSCode (5 messages, latest: Apr 21 2021 at 22:53)
- addDeclarationRanges eval taking forever (14 messages, latest: Apr 20 2021 at 20:13)
- Dependent Pattern Matching (11 messages, latest: Apr 20 2021 at 08:34)
- New tags in the lean4 github repo (1 message, latest: Apr 19 2021 at 18:30)
- Community Guidelines (1 message, latest: Apr 19 2021 at 16:13)
- Missing
mkCharLit
(1 message, latest: Apr 18 2021 at 20:06) - simp and bundled structure (1 message, latest: Apr 17 2021 at 04:53)
- Macro expand to hypotheses (11 messages, latest: Apr 16 2021 at 19:26)
- Lean.Name DecidableEq (15 messages, latest: Apr 16 2021 at 12:07)
- mathlib:prelude (27 messages, latest: Apr 16 2021 at 00:13)
- Unable to update lean4 version (7 messages, latest: Apr 15 2021 at 16:47)
- mathlib:delab (69 messages, latest: Apr 15 2021 at 15:48)
- mathlib:namespace (2 messages, latest: Apr 15 2021 at 07:42)
- Custom identifiers? (21 messages, latest: Apr 15 2021 at 07:20)
- parenthesizer backtrack errors? (5 messages, latest: Apr 14 2021 at 18:14)
- Beginner questions (89 messages, latest: Apr 13 2021 at 20:28)
- build simp syntax? (3 messages, latest: Apr 13 2021 at 17:27)
- Proving findLeast: an experience report (155 messages, latest: Apr 13 2021 at 16:30)
- implicit lambdas (2 messages, latest: Apr 13 2021 at 16:27)
- lean4 vscode setup? (17 messages, latest: Apr 12 2021 at 16:50)
- elab not implemented picks up comments (5 messages, latest: Apr 12 2021 at 16:31)
- panic in quotation parsing (2 messages, latest: Apr 12 2021 at 16:08)
- panic in macro_rules attributes (3 messages, latest: Apr 12 2021 at 16:07)
- Lean4 and multidimensional arrays (14 messages, latest: Apr 12 2021 at 15:26)
- olean files to source (7 messages, latest: Apr 12 2021 at 10:57)
- can't print unit (9 messages, latest: Apr 12 2021 at 10:18)
- unreachable code panic (1 message, latest: Apr 12 2021 at 05:53)
- mathport:numbers (53 messages, latest: Apr 10 2021 at 03:43)
- Neovim support (12 messages, latest: Apr 09 2021 at 02:06)
- tip for nested/mutual inductive types? (6 messages, latest: Apr 08 2021 at 20:50)
- lean_expr_mk (3 messages, latest: Apr 08 2021 at 18:02)
- Lean should update flake.lock file (4 messages, latest: Apr 08 2021 at 13:01)
- Postfix operator precedence issue (4 messages, latest: Apr 07 2021 at 21:36)
- coercion/inference pitfall (3 messages, latest: Apr 07 2021 at 18:00)
- Postfix operator precendence issue (4 messages, latest: Apr 07 2021 at 07:20)
- Smart unfolding produces ununfoldable terms (2 messages, latest: Apr 07 2021 at 01:24)
- elab goals for concrete arith (10 messages, latest: Apr 06 2021 at 00:39)
- Induction issue? (2 messages, latest: Apr 03 2021 at 17:43)
- instance priorities (2 messages, latest: Apr 02 2021 at 16:36)
- Subsingleton.elim (2 messages, latest: Apr 02 2021 at 16:08)
- mathport:tags (3 messages, latest: Apr 02 2021 at 02:56)
- Guidelines on coercion instances (10 messages, latest: Apr 01 2021 at 17:41)
- Theorem Names (10 messages, latest: Mar 31 2021 at 22:34)
- lean4-balance-car (5 messages, latest: Mar 30 2021 at 23:39)
Option
always open? (5 messages, latest: Mar 30 2021 at 22:57)- golfing Subsingleton Empty (7 messages, latest: Mar 30 2021 at 22:12)
- Implicit arguments and pattern matching (5 messages, latest: Mar 30 2021 at 16:05)
- mathlib (110 messages, latest: Mar 27 2021 at 22:48)
- Root Exports (1 message, latest: Mar 27 2021 at 18:43)
- or-patterns in match expressions (5 messages, latest: Mar 27 2021 at 18:32)
- Lean Protobuf (2 messages, latest: Mar 27 2021 at 16:57)
- vscode-lean4 Doesn't Work When I Switch Files (4 messages, latest: Mar 26 2021 at 20:07)
- apply and term mode unfolding (13 messages, latest: Mar 26 2021 at 01:35)
- missing tactics (19 messages, latest: Mar 25 2021 at 14:42)
- argv[0] (3 messages, latest: Mar 25 2021 at 14:31)
- string literal containing comment character (5 messages, latest: Mar 24 2021 at 20:11)
- refine tactic syntax for inductive types (7 messages, latest: Mar 24 2021 at 05:48)
- Constant-stack monadic loops (15 messages, latest: Mar 24 2021 at 02:39)
- expanding cases syntax (9 messages, latest: Mar 23 2021 at 19:15)
- mathport:sunfold (25 messages, latest: Mar 23 2021 at 17:34)
- Viewing IR? (6 messages, latest: Mar 23 2021 at 07:51)
- VSCode cross file synchronization (10 messages, latest: Mar 22 2021 at 23:06)
- Reducibility and Classes (8 messages, latest: Mar 22 2021 at 22:48)
- design decisions around type inference and elaboration (5 messages, latest: Mar 22 2021 at 21:58)
- PR welcome? (21 messages, latest: Mar 22 2021 at 21:42)
- decidable equality instances (4 messages, latest: Mar 22 2021 at 19:08)
- tab completion? (2 messages, latest: Mar 22 2021 at 18:41)
- strange printing of set_option in (1 message, latest: Mar 22 2021 at 18:36)
- autoindentation? (1 message, latest: Mar 22 2021 at 18:35)
- pure IO (29 messages, latest: Mar 22 2021 at 14:48)
- deriving ToString? (3 messages, latest: Mar 22 2021 at 14:31)
- Creating Lean environment (8 messages, latest: Mar 22 2021 at 11:13)
- state of the vscode extension (8 messages, latest: Mar 21 2021 at 13:37)
- mathport:whnf-power (12 messages, latest: Mar 20 2021 at 23:32)
- mathport:instExpected (10 messages, latest: Mar 20 2021 at 23:03)
- Updating structure fields (6 messages, latest: Mar 20 2021 at 21:57)
- Inductive definition in macros (28 messages, latest: Mar 20 2021 at 21:42)
- variables v subtype (6 messages, latest: Mar 20 2021 at 17:51)
- mathport:synth (60 messages, latest: Mar 20 2021 at 15:47)
- system interaction? (5 messages, latest: Mar 19 2021 at 22:26)
- unknown package 'Init' (14 messages, latest: Mar 19 2021 at 22:25)
- reducible instances (3 messages, latest: Mar 19 2021 at 21:40)
- leanpkg build bin with dependencies (2 messages, latest: Mar 19 2021 at 20:41)
- leanpkg add? (1 message, latest: Mar 19 2021 at 19:00)
- command line argument parsing (3 messages, latest: Mar 19 2021 at 18:53)
- reusing the Lean compiler in my program? (3 messages, latest: Mar 19 2021 at 16:46)
- def root.foo ? (5 messages, latest: Mar 19 2021 at 15:51)
- merging namespaces? (7 messages, latest: Mar 19 2021 at 15:10)
- mathport:irreducible (68 messages, latest: Mar 19 2021 at 15:04)
- How to mactch an operator in Macro_rules (14 messages, latest: Mar 19 2021 at 11:09)
- Benchmarks for Lean 4 (8 messages, latest: Mar 18 2021 at 14:04)
- Nested
sepBy
(17 messages, latest: Mar 18 2021 at 09:14) - Code generation (19 messages, latest: Mar 17 2021 at 21:36)
- simp databases (13 messages, latest: Mar 17 2021 at 18:24)
- leanpkg ignores (37 messages, latest: Mar 17 2021 at 11:44)
- Mathlib on Lean4 when? (9 messages, latest: Mar 17 2021 at 04:01)
- Unnecessary Inhabited constraint on Array.modified (7 messages, latest: Mar 16 2021 at 16:34)
- Notation in structures (33 messages, latest: Mar 16 2021 at 14:01)
- Structure Extensions (3 messages, latest: Mar 16 2021 at 08:23)
- issues with "import" (5 messages, latest: Mar 16 2021 at 07:01)
- deep structural recursion was detected (2 messages, latest: Mar 16 2021 at 02:19)
- tracing unification? (3 messages, latest: Mar 15 2021 at 21:52)
- unterminated comments (3 messages, latest: Mar 15 2021 at 17:59)
- local notations (9 messages, latest: Mar 15 2021 at 17:48)
- HasEquiv in Type? (5 messages, latest: Mar 15 2021 at 17:48)
- Custom intro (3 messages, latest: Mar 14 2021 at 01:10)
- Is nested pattern matching not possible? (3 messages, latest: Mar 13 2021 at 22:40)
- unfolding in typeclass instance search? (3 messages, latest: Mar 13 2021 at 04:12)
- outparam classes (6 messages, latest: Mar 13 2021 at 03:08)
- have with metavariables? (13 messages, latest: Mar 13 2021 at 03:06)
- Default instances (25 messages, latest: Mar 13 2021 at 02:59)
- banning
!
suffix from keywords (1 message, latest: Mar 13 2021 at 02:19) - tracing typeclasses? (3 messages, latest: Mar 12 2021 at 20:40)
- function coercions in the stdlib (5 messages, latest: Mar 12 2021 at 20:29)
- set_option list (5 messages, latest: Mar 12 2021 at 20:18)
- Surprising syntax error (24 messages, latest: Mar 12 2021 at 19:27)
- How does the attribute actually works? (1 message, latest: Mar 12 2021 at 16:02)
- coeSort? (8 messages, latest: Mar 12 2021 at 15:44)
- overloading pairing notation (7 messages, latest: Mar 12 2021 at 15:22)
- lean4-mode C-c C-n? (7 messages, latest: Mar 11 2021 at 22:12)
- lean4-mode: minor quality-of-life feature request (1 message, latest: Mar 11 2021 at 22:09)
- OfNat Type vs. Sort (1 message, latest: Mar 11 2021 at 21:31)
- unfortunate error messages (3 messages, latest: Mar 11 2021 at 20:43)
- binding scopes to notations? (5 messages, latest: Mar 11 2021 at 20:38)
- Is seeing sorryAx a bug? (2 messages, latest: Mar 11 2021 at 20:19)
- Prop Def? (5 messages, latest: Mar 11 2021 at 17:17)
- Go-to-definition in the standard library (7 messages, latest: Mar 11 2021 at 13:02)
- "invalid mutual block" (4 messages, latest: Mar 10 2021 at 23:20)
- defining notations and structures simultaneously (2 messages, latest: Mar 10 2021 at 20:46)
- significance of (kernel) in error messages? (4 messages, latest: Mar 10 2021 at 15:25)
- amusing (6 messages, latest: Mar 09 2021 at 05:17)
- invalid patterns from local variables (2 messages, latest: Mar 08 2021 at 16:37)
- nested patterns in cases? (4 messages, latest: Mar 08 2021 at 14:43)
- simplify the context of a hole before displaying it? (3 messages, latest: Mar 08 2021 at 14:11)
- Subtypes (5 messages, latest: Mar 08 2021 at 11:21)
- Int.negSucc (13 messages, latest: Mar 07 2021 at 21:11)
- variable/variables/universe/universes (7 messages, latest: Mar 07 2021 at 08:31)
- doc additions (1 message, latest: Mar 06 2021 at 19:20)
- expected type sorry? (3 messages, latest: Mar 06 2021 at 15:43)
- error: binary package was not provided for 'linux' (3 messages, latest: Mar 06 2021 at 00:40)
- tracking down apparent de Bruijn indexing bugs? (1 message, latest: Mar 05 2021 at 21:38)
- Accessing shadowed top-level definitions (6 messages, latest: Mar 05 2021 at 19:54)
- local open / let open (2 messages, latest: Mar 05 2021 at 18:42)
- how does "proofs for performance and profit" work? (3 messages, latest: Mar 05 2021 at 11:34)
- stage0 (3 messages, latest: Mar 04 2021 at 15:37)
- desugar mut variables (2 messages, latest: Mar 04 2021 at 11:40)
- Is there a way to build proof interactively (3 messages, latest: Mar 04 2021 at 03:41)
- match syntax sugar (22 messages, latest: Mar 04 2021 at 03:16)
- OfNat (5 messages, latest: Mar 02 2021 at 18:57)
- Compiling to C (4 messages, latest: Mar 02 2021 at 16:33)
- determine whether type is enumerated (3 messages, latest: Mar 02 2021 at 06:00)
- modeling "simple" recursive datatypes (1 message, latest: Feb 28 2021 at 17:28)
- mixing positional and keyword arguments (3 messages, latest: Feb 27 2021 at 21:49)
- Tactic for absurdity (4 messages, latest: Feb 26 2021 at 00:29)
- getting started with Lean 4 (26 messages, latest: Feb 25 2021 at 09:24)
- How to setup lean4 vscode extension (17 messages, latest: Feb 24 2021 at 15:21)
- How to setup lean4 viscose extension (3 messages, latest: Feb 24 2021 at 09:34)
- bitwise operations on
USize
(23 messages, latest: Feb 24 2021 at 08:08) - Trying to get simple example to compile (31 messages, latest: Feb 23 2021 at 14:02)
- clean syntax for initializing associative lists? (5 messages, latest: Feb 21 2021 at 23:02)
open
at end of file (1 message, latest: Feb 21 2021 at 18:49)- jump to definition (1 message, latest: Feb 21 2021 at 17:49)
- СamelСase (4 messages, latest: Feb 21 2021 at 09:14)
- Testing (3 messages, latest: Feb 21 2021 at 01:35)
- What's "@&" in external function defination? (4 messages, latest: Feb 20 2021 at 10:15)
- From/ToJson for user code (4 messages, latest: Feb 20 2021 at 00:05)
- mathport (199 messages, latest: Feb 18 2021 at 03:26)
- Missing nightly (5 messages, latest: Feb 12 2021 at 21:56)
- congr lemmas for ite/dite (1 message, latest: Feb 12 2021 at 09:34)
- System programming using Lean 4 (20 messages, latest: Feb 11 2021 at 19:10)
- tactic to equate inductive indices (14 messages, latest: Feb 11 2021 at 14:41)
- Unexpected overloading with export command (20 messages, latest: Feb 10 2021 at 17:50)
- syntax and elaboration functions are nowhere near each other (3 messages, latest: Feb 10 2021 at 08:25)
- MetaM behaviour in vscode-lean4 (10 messages, latest: Feb 06 2021 at 08:32)
- end a reopened namespace (6 messages, latest: Feb 05 2021 at 20:41)
- microcalc (19 messages, latest: Feb 05 2021 at 10:53)
- ring (12 messages, latest: Feb 05 2021 at 03:04)
- type mismatch error (45 messages, latest: Feb 04 2021 at 23:59)
- structured tracing (11 messages, latest: Feb 04 2021 at 20:07)
- Failed to show type is inhabited (6 messages, latest: Feb 04 2021 at 06:07)
- opposite (3 messages, latest: Feb 03 2021 at 19:42)
- expr pattern matching (22 messages, latest: Feb 03 2021 at 18:04)
- dependencies (16 messages, latest: Feb 03 2021 at 16:13)
- "..s" in structure literals (2 messages, latest: Feb 02 2021 at 17:47)
- expr.local_const (9 messages, latest: Feb 02 2021 at 16:57)
- lean4 repo in vscode (39 messages, latest: Feb 02 2021 at 16:55)
- fun with syntax ambiguity (18 messages, latest: Feb 02 2021 at 10:38)
- declaration has metavariables (4 messages, latest: Feb 01 2021 at 23:31)
- Assertion failure due to LEAN_MAX_SMALL_OBJECT_SIZE (7 messages, latest: Feb 01 2021 at 22:21)
- infix completion (2 messages, latest: Feb 01 2021 at 20:45)
- Raw do notation (17 messages, latest: Feb 01 2021 at 05:52)
- Profiling (17 messages, latest: Feb 01 2021 at 01:57)
- Contradiction? (24 messages, latest: Jan 31 2021 at 16:36)
- Nightly 01-31 (4 messages, latest: Jan 31 2021 at 01:34)
- injection error (2 messages, latest: Jan 30 2021 at 20:01)
- lemma (70 messages, latest: Jan 29 2021 at 10:19)
- port34 (3 messages, latest: Jan 29 2021 at 09:57)
- simp instance trace (2 messages, latest: Jan 29 2021 at 08:42)
- Home of vscode-lean4 (101 messages, latest: Jan 29 2021 at 06:34)
- Unsafe proofs (3 messages, latest: Jan 29 2021 at 00:36)
- Tactics (8 messages, latest: Jan 28 2021 at 23:30)
- monad performance (17 messages, latest: Jan 28 2021 at 20:00)
- noncomputable/irrelevant fields (6 messages, latest: Jan 28 2021 at 17:16)
- parens on method LHS (19 messages, latest: Jan 28 2021 at 17:16)
- abbreviation issue (9 messages, latest: Jan 28 2021 at 07:02)
- root (4 messages, latest: Jan 27 2021 at 16:36)
- Compilation backend (5 messages, latest: Jan 26 2021 at 10:09)
- Comment on my extension request (9 messages, latest: Jan 26 2021 at 09:59)
- build issue (3 messages, latest: Jan 25 2021 at 21:39)
- Negation and Floats (Is
Neg.neg
biased towardsInt
?) (3 messages, latest: Jan 25 2021 at 21:30) - Documentation (1 message, latest: Jan 25 2021 at 19:49)
- Compile Lean code to a neat little executable (8 messages, latest: Jan 25 2021 at 16:22)
- leanpkg configure (15 messages, latest: Jan 25 2021 at 15:52)
- Web Programming with Lean 4 (41 messages, latest: Jan 25 2021 at 15:00)
- deriving extensions (1 message, latest: Jan 25 2021 at 04:20)
List.map
preserves length (2 messages, latest: Jan 25 2021 at 04:08)elan default ...
hangs (6 messages, latest: Jan 24 2021 at 18:37)- How do I install vscode-lean4? (17 messages, latest: Jan 24 2021 at 14:02)
- Induction on Dependent Pairs (3 messages, latest: Jan 23 2021 at 02:38)
- functional but in place paradigm (13 messages, latest: Jan 23 2021 at 01:47)
- interweave proof and code (5 messages, latest: Jan 22 2021 at 15:39)
- Some idea about syntax (3 messages, latest: Jan 18 2021 at 00:02)
- plans for network programming API (7 messages, latest: Jan 17 2021 at 22:32)
- deriving (1 message, latest: Jan 17 2021 at 20:48)
- plans for Socket API (3 messages, latest: Jan 17 2021 at 15:02)
- Coding with Lean 4 (10 messages, latest: Jan 15 2021 at 03:40)
- Typeclass inference diamond (5 messages, latest: Jan 14 2021 at 02:50)
- Casting Float to some integral type (4 messages, latest: Jan 13 2021 at 17:07)
- contributing (3 messages, latest: Jan 13 2021 at 12:43)
induction
tactic (8 messages, latest: Jan 12 2021 at 15:32)- OfNat abbreviation (2 messages, latest: Jan 12 2021 at 15:00)
- pattern variable issue? (3 messages, latest: Jan 12 2021 at 14:45)
- metavariables in lemma statements (7 messages, latest: Jan 12 2021 at 00:50)
- unification hint (21 messages, latest: Jan 10 2021 at 15:48)
- qsort with >= (3 messages, latest: Jan 10 2021 at 12:22)
- AssocList "failed to synthesize" (8 messages, latest: Jan 10 2021 at 12:15)
- Porting Mathlib: Style Changes (17 messages, latest: Jan 10 2021 at 04:00)
- Some links (2 messages, latest: Jan 10 2021 at 03:41)
- simple performance testing (52 messages, latest: Jan 09 2021 at 21:01)
- Elaboration Strategies (2 messages, latest: Jan 09 2021 at 14:09)
- Meetings with Leo (11 messages, latest: Jan 08 2021 at 20:54)
- Possible bug? (9 messages, latest: Jan 08 2021 at 19:36)
- Nightlies (1 message, latest: Jan 08 2021 at 10:38)
- Porting Mathlib: Essential Changes (17 messages, latest: Jan 08 2021 at 10:10)
- Attribute specialize (13 messages, latest: Jan 08 2021 at 09:40)
- Pattern matching limitations? (4 messages, latest: Jan 08 2021 at 09:39)
- capitalization (7 messages, latest: Jan 07 2021 at 12:06)
- coercion (1 message, latest: Jan 07 2021 at 08:39)
- outdated (3 messages, latest: Jan 07 2021 at 08:26)
- How to run
main
? (1 message, latest: Jan 06 2021 at 21:49) - How to install Lean 4? (10 messages, latest: Jan 06 2021 at 18:08)
- arbitrary is a constant (17 messages, latest: Jan 06 2021 at 12:51)
- Lean 4 ecosystem (1 message, latest: Jan 06 2021 at 01:31)
- vim support? (18 messages, latest: Jan 05 2021 at 21:46)
- [Sort ](topic/Sort.20.html) (10 messages, latest: Jan 05 2021 at 21:36)
- by apply_instance (3 messages, latest: Jan 05 2021 at 21:10)
- How to indicate empty matches in Lean 4 (15 messages, latest: Jan 05 2021 at 20:51)
apply
bug? (8 messages, latest: Jan 05 2021 at 20:39)- Constructors are injective? (12 messages, latest: Jan 05 2021 at 20:19)
- cleaning your hard disk (3 messages, latest: Jan 05 2021 at 19:39)
- VSCode error message (7 messages, latest: Jan 05 2021 at 15:52)
- update (1 message, latest: Jan 05 2021 at 15:41)
- #help (3 messages, latest: Jan 05 2021 at 13:01)
- quotient (1 message, latest: Jan 05 2021 at 12:50)
Last updated: Jan 31 2023 at 21:29 UTC