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 structures? (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 ;/<;> vs try/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 vs Std.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 problems~~ reverting 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 with abbrev (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 problems~~ reverting 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 for buildLeanPackage (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 of isInr (2 messages, latest: Sep 20 2022 at 19:14)
Extracting inr having a proof of isInr (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 a TacticM 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 and import 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 not whnf (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 and Applicative (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 vs has_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 - producesapplication type mismatch (1 message, latest: Oct 18 2021 at 22:19)
Simp bug - producesapplication 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 ites (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 towards Int?) (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