Zulip Chat Archive

Stream: mathlib4

Topics:

Finite set over infinite type (10 messages, latest: Jan 31 2023 at 21:27)
deprecated lean3-ism convention (22 messages, latest: Jan 31 2023 at 21:13)
count_eq_card_filter_eq (29 messages, latest: Jan 31 2023 at 18:54)
Data.Finset.Pointwise !4#1911 (1 message, latest: Jan 31 2023 at 18:51)
align bool,option,list,nat (1 message, latest: Jan 31 2023 at 18:39)
port progress (1926 messages, latest: Jan 31 2023 at 18:35)
olympiad problems with mathlib4 (32 messages, latest: Jan 31 2023 at 17:34)
Tactic porting assignments (320 messages, latest: Jan 31 2023 at 15:26)
port benchmark (187 messages, latest: Jan 31 2023 at 15:20)
restart port (2 messages, latest: Jan 31 2023 at 15:10)
casesm changed behaviour !4#1744 (4 messages, latest: Jan 31 2023 at 13:11)
names distinguished only by case (48 messages, latest: Jan 31 2023 at 11:38)
New Project that uses MathLib4 (107 messages, latest: Jan 31 2023 at 11:29)
✔ Quote4 and tactics (8 messages, latest: Jan 31 2023 at 10:20)
add missing #align statements !4#1966 (6 messages, latest: Jan 31 2023 at 09:29)
Can't find instance (3 messages, latest: Jan 31 2023 at 08:00)
finding simps lemmas (20 messages, latest: Jan 30 2023 at 23:55)
open classical (8 messages, latest: Jan 30 2023 at 22:38)
GroupTheory.Coset !4#1874 (3 messages, latest: Jan 30 2023 at 22:30)
unknown free variable (36 messages, latest: Jan 30 2023 at 22:23)
Data.Finsupp.Basic !4#1949 (1 message, latest: Jan 30 2023 at 22:06)
expected command, expected :=, expected structure (11 messages, latest: Jan 30 2023 at 20:12)
notation overloading linter (1 message, latest: Jan 30 2023 at 19:32)
to_additive for generated lemmas (18 messages, latest: Jan 30 2023 at 16:51)
✔ RingTheory.Subsemiring.Basic !4#1862 (5 messages, latest: Jan 30 2023 at 12:09)
✔ Algebra.GradedMulAction (4 messages, latest: Jan 30 2023 at 10:21)
OfScientific (96 messages, latest: Jan 30 2023 at 06:36)
obtain to massage syntactic equality (4 messages, latest: Jan 30 2023 at 06:06)
simp priority (3 messages, latest: Jan 30 2023 at 04:59)
RatCast ℚ instance (2 messages, latest: Jan 30 2023 at 02:59)
linarith failure (23 messages, latest: Jan 29 2023 at 22:56)
Singleton notation (9 messages, latest: Jan 29 2023 at 22:17)
GroupTheory.GroupAction.SubMulAction.Pointwise (15 messages, latest: Jan 29 2023 at 15:48)
removal of command line for teaching (15 messages, latest: Jan 29 2023 at 15:40)
tagged releases? (39 messages, latest: Jan 29 2023 at 11:05)
calc blocks and heterogeneous operators (16 messages, latest: Jan 29 2023 at 08:49)
simplifying "dependent" match (1 message, latest: Jan 29 2023 at 07:11)
"(kernel) declaration has metavariables" (45 messages, latest: Jan 29 2023 at 06:13)
CoeFun (33 messages, latest: Jan 29 2023 at 03:32)
add missing #align statements !4#1902 (4 messages, latest: Jan 29 2023 at 01:45)
macro_rules with an argument (29 messages, latest: Jan 28 2023 at 22:17)
data.analysis (8 messages, latest: Jan 28 2023 at 21:48)
feat: port Algebra.BigOperators.Intervals (3 messages, latest: Jan 28 2023 at 19:18)
tfae Tfae TFEA (13 messages, latest: Jan 28 2023 at 17:41)
lake get-cache (652 messages, latest: Jan 28 2023 at 11:50)
simpNF claims LHS doesn't simplify, but it does (14 messages, latest: Jan 28 2023 at 06:54)
Lots of 1 + 1 + 1 + 1 (20 messages, latest: Jan 28 2023 at 05:35)
Mathport oneshot (94 messages, latest: Jan 28 2023 at 03:43)
another rat reducibility issue? (6 messages, latest: Jan 28 2023 at 02:46)
Instance transparency issue? (28 messages, latest: Jan 28 2023 at 02:10)
What is an outParam? (65 messages, latest: Jan 28 2023 at 01:21)
unification weaker in lean4 (15 messages, latest: Jan 28 2023 at 01:13)
coercion from PNat to Rat (5 messages, latest: Jan 27 2023 at 22:08)
porters (27 messages, latest: Jan 27 2023 at 21:56)
Making variable in class field explicit (16 messages, latest: Jan 27 2023 at 19:10)
Push access (19 messages, latest: Jan 27 2023 at 17:34)
Rogue Int.ofNat maxing out recursion depth for decimals (8 messages, latest: Jan 27 2023 at 17:29)
Combinatorics.SimpleGraph.Basic mathlib4#1883 (1 message, latest: Jan 27 2023 at 16:53)
Data.Dfinsupp.Basic !4#1829 (17 messages, latest: Jan 27 2023 at 15:48)
simpNF problems (10 messages, latest: Jan 27 2023 at 14:26)
✔ Group instance (6 messages, latest: Jan 27 2023 at 13:53)
Data.Finsupp.Defs mathlib4#1807 (43 messages, latest: Jan 27 2023 at 12:57)
reducible non-instances (2 messages, latest: Jan 27 2023 at 11:42)
GroupTheory.FreeGroup mathlib4#1867 (28 messages, latest: Jan 27 2023 at 11:09)
GroupTheory.GroupAction.ConjAct !4#1871 (6 messages, latest: Jan 27 2023 at 09:49)
failed to synthesize Additive (Group G) (2 messages, latest: Jan 27 2023 at 03:36)
DiscreteTopology bot (11 messages, latest: Jan 27 2023 at 02:13)
Mathlib4 porting meeting series (183 messages, latest: Jan 27 2023 at 00:54)
simp under binders (16 messages, latest: Jan 26 2023 at 23:06)
Diamond issue in Algebra.Star.Basic (9 messages, latest: Jan 26 2023 at 22:22)
weird interaction between mod_cases and induction (12 messages, latest: Jan 26 2023 at 21:53)
use tactic is no longer finishing (7 messages, latest: Jan 26 2023 at 21:01)
documented high level porting procedure in the wiki (2 messages, latest: Jan 26 2023 at 20:15)
Algebra.Star.SelfAdjoint !4#1860 (1 message, latest: Jan 26 2023 at 19:05)
Missing lemmas (9 messages, latest: Jan 26 2023 at 18:51)
to_additive type mismatch (7 messages, latest: Jan 26 2023 at 17:13)
Algebra.Module.Equiv mathlib4#1732 (44 messages, latest: Jan 26 2023 at 14:33)
GroupTheory.Subgroup.Basic !4#1797 (12 messages, latest: Jan 26 2023 at 09:39)
Order.Filter.Pointwise !4#1839 (1 message, latest: Jan 26 2023 at 04:29)
Topology.Tactic (4 messages, latest: Jan 26 2023 at 00:17)
unassigned metavariable in out-param (7 messages, latest: Jan 25 2023 at 21:45)
Topology.Basic !4#1826 (11 messages, latest: Jan 25 2023 at 19:53)
Naming convention (46 messages, latest: Jan 25 2023 at 17:31)
Topology.Bornology.Basic (13 messages, latest: Jan 25 2023 at 15:48)
Order.LocallyFinite !4#1754 (12 messages, latest: Jan 25 2023 at 12:20)
Order.Hom.Lattice (33 messages, latest: Jan 25 2023 at 12:09)
mathlib4#1777 (1 message, latest: Jan 25 2023 at 07:58)
✔ epsilon (3 messages, latest: Jan 25 2023 at 06:06)
Bikeshedding: Data.Seq.Seq (15 messages, latest: Jan 25 2023 at 00:27)
to_additive with inductive (7 messages, latest: Jan 24 2023 at 22:00)
Infer kinds are unsupported (10 messages, latest: Jan 24 2023 at 20:13)
Algebra.Quandle held up by group (5 messages, latest: Jan 24 2023 at 19:43)
attr := simp (17 messages, latest: Jan 24 2023 at 19:31)
syntax matches when literal doesn't (4 messages, latest: Jan 24 2023 at 17:30)
to_additive align failures (54 messages, latest: Jan 24 2023 at 16:55)
✔ nonrec vs root (79 messages, latest: Jan 24 2023 at 16:25)
non-aligned definitions (40 messages, latest: Jan 24 2023 at 15:17)
conv (2 messages, latest: Jan 24 2023 at 13:54)
data.bitvec.core mathlib4#1731 (10 messages, latest: Jan 24 2023 at 13:14)
introducing docstrings while porting (14 messages, latest: Jan 24 2023 at 11:51)
synport experimentation (105 messages, latest: Jan 24 2023 at 11:24)
order.filter.germ (12 messages, latest: Jan 24 2023 at 11:08)
decidable/classical (4 messages, latest: Jan 24 2023 at 09:13)
✔ port Data.LazyList.Basic (12 messages, latest: Jan 24 2023 at 08:15)
linkifier (4 messages, latest: Jan 24 2023 at 08:06)
Order.Filter.NAry (17 messages, latest: Jan 24 2023 at 05:19)
bug in linarith (14 messages, latest: Jan 24 2023 at 03:02)
order.filter.at_top_bot (3 messages, latest: Jan 24 2023 at 02:00)
Data.Pfun Issues Summary ( mathlib4#1179) (2 messages, latest: Jan 23 2023 at 23:32)
mathport root (17 messages, latest: Jan 23 2023 at 20:08)
align private decls (20 messages, latest: Jan 23 2023 at 19:02)
Set.mem_setOf_eq (7 messages, latest: Jan 23 2023 at 16:55)
data.fin.vec_notation mathlib4#1741 (21 messages, latest: Jan 23 2023 at 16:45)
Algebra.BigOperators.Finprod mathlib4#1766 (11 messages, latest: Jan 23 2023 at 16:34)
auto-fix comments (10 messages, latest: Jan 23 2023 at 15:16)
[meta] avoiding multiple environments (6 messages, latest: Jan 23 2023 at 15:05)
to_additive translating pow to nsmul (10 messages, latest: Jan 23 2023 at 13:44)
elab_as_elim (5 messages, latest: Jan 23 2023 at 13:38)
✔ to_additive.map_namespace (7 messages, latest: Jan 23 2023 at 12:53)
Remove a file from PR (24 messages, latest: Jan 23 2023 at 11:57)
mathport issues (41 messages, latest: Jan 23 2023 at 09:42)
linarith error in structured proof (8 messages, latest: Jan 23 2023 at 09:41)
Union notation (2 messages, latest: Jan 23 2023 at 08:23)
lift_pair etc (3 messages, latest: Jan 23 2023 at 08:22)
slow positivity (35 messages, latest: Jan 23 2023 at 04:46)
linarith with discharger (8 messages, latest: Jan 23 2023 at 04:06)
order.filter.basic (39 messages, latest: Jan 23 2023 at 02:48)
nontriviality leaves metavars (6 messages, latest: Jan 22 2023 at 23:07)
ring vs Ring (17 messages, latest: Jan 22 2023 at 20:46)
induction, case, rcases (8 messages, latest: Jan 22 2023 at 18:54)
Linter complains about porting note before docstring (3 messages, latest: Jan 22 2023 at 18:27)
Port Order/OrderIsoNat (22 messages, latest: Jan 22 2023 at 17:18)
Issues importing mathlib4 (57 messages, latest: Jan 22 2023 at 16:31)
[field_simp] simp timeout (45 messages, latest: Jan 22 2023 at 08:56)
making a TacticM (24 messages, latest: Jan 22 2023 at 07:07)
unusedVariables (39 messages, latest: Jan 22 2023 at 06:54)
default "/" meaning (22 messages, latest: Jan 21 2023 at 10:33)
Data.Set.Finite mathlib4#1734 (47 messages, latest: Jan 21 2023 at 03:25)
norm_num yielding 1/1 (1 message, latest: Jan 21 2023 at 03:08)
alias & protected (10 messages, latest: Jan 21 2023 at 01:28)
congr tactic hitting max recursion depth (13 messages, latest: Jan 21 2023 at 01:02)
my PRs that need help (22 messages, latest: Jan 21 2023 at 00:04)
Logic.Equiv.Array (5 messages, latest: Jan 20 2023 at 23:11)
[CI] error getting cache (51 messages, latest: Jan 20 2023 at 19:51)
Port Status Webpage (47 messages, latest: Jan 20 2023 at 19:05)
Data.Fintype.Vector mathlib4#1716 (42 messages, latest: Jan 20 2023 at 18:29)
✔ cast_sub in ring (11 messages, latest: Jan 20 2023 at 16:41)
import name changes (1 message, latest: Jan 20 2023 at 16:41)
Data.SetLike.Fintype mathlib4#1727 (6 messages, latest: Jan 20 2023 at 16:25)
how to port? (35 messages, latest: Jan 20 2023 at 15:48)
BigOperators parsing precedence (14 messages, latest: Jan 20 2023 at 15:21)
algebra.module.linear_map mathlib4#1587 (8 messages, latest: Jan 20 2023 at 14:10)
Data.Zmod.Defs mathlib4#1713 (3 messages, latest: Jan 20 2023 at 13:02)
Data.Sym.Basic mathlib4#1672 (10 messages, latest: Jan 20 2023 at 09:21)
norm_num characteristic functionality (55 messages, latest: Jan 20 2023 at 08:51)
Data.Nat.Factors mathlib4#1664 (8 messages, latest: Jan 20 2023 at 04:58)
New solve_by_elim (43 messages, latest: Jan 20 2023 at 01:06)
enat (19 messages, latest: Jan 19 2023 at 23:31)
Instance naming for Equiv instances (2 messages, latest: Jan 19 2023 at 21:13)
Potential Bug in symm tactic (23 messages, latest: Jan 19 2023 at 19:58)
starting the port of a new file (68 messages, latest: Jan 19 2023 at 19:09)
strange type issue in mathlib4#1685 (5 messages, latest: Jan 19 2023 at 19:02)
warning: expanding binder collection (2 messages, latest: Jan 19 2023 at 18:58)
start_port.sh fails (54 messages, latest: Jan 19 2023 at 18:17)
Invalid auto and opt values (1 message, latest: Jan 19 2023 at 17:24)
unusedArguments (1 message, latest: Jan 19 2023 at 16:53)
data.nat.fib mathlib4#1644 (63 messages, latest: Jan 19 2023 at 15:39)
Linter complains about let rec missing docstring (9 messages, latest: Jan 19 2023 at 14:59)
Hypothesis renaming — mathlib4#1658 (12 messages, latest: Jan 19 2023 at 14:13)
zify bugs? (6 messages, latest: Jan 19 2023 at 12:38)
Updating SHAs for modified files (7 messages, latest: Jan 19 2023 at 12:25)
finset.sum_smul (3 messages, latest: Jan 19 2023 at 11:43)
Data.Finset.Sups mathlib4#1663 (14 messages, latest: Jan 19 2023 at 10:41)
Data.Fin.Tuple.Basic mathlib4#1516 (35 messages, latest: Jan 19 2023 at 09:10)
congr and subsingleton.elim (1 message, latest: Jan 19 2023 at 08:06)
change … with replacement (2 messages, latest: Jan 18 2023 at 20:10)
generalized functions of Fin n? (17 messages, latest: Jan 18 2023 at 19:36)
help wanted porting Algebra.Order.Module (3 messages, latest: Jan 18 2023 at 19:03)
bit0 deprecated (37 messages, latest: Jan 18 2023 at 16:37)
setOf unexpander (7 messages, latest: Jan 18 2023 at 16:26)
Prop -> Bool regression (52 messages, latest: Jan 18 2023 at 15:41)
Computable Fin Induction (7 messages, latest: Jan 18 2023 at 14:52)
open_locale big_operators (6 messages, latest: Jan 18 2023 at 14:38)
Algebra.BigOperators.Basic mathlib4#1628 (16 messages, latest: Jan 18 2023 at 13:20)
@[simp] on equation compiler definitions (64 messages, latest: Jan 18 2023 at 13:09)
indentation, by (10 messages, latest: Jan 18 2023 at 11:26)
Meaning of specialize (9 messages, latest: Jan 18 2023 at 09:45)
mathlib3port not updating (11 messages, latest: Jan 18 2023 at 08:58)
Using List.get in Vector.Basic (27 messages, latest: Jan 18 2023 at 07:42)
data.finmap mathlib4#1591 (26 messages, latest: Jan 18 2023 at 01:38)
matching a non-merged mathlib3 PR (3 messages, latest: Jan 18 2023 at 00:25)
recursive ext in Lean 4? (8 messages, latest: Jan 17 2023 at 23:21)
DecidableLE for Finset (7 messages, latest: Jan 17 2023 at 22:37)
Order.OmegaCompletePartialOrder mathlib4#1168 (7 messages, latest: Jan 17 2023 at 19:04)
convert failures (3 messages, latest: Jan 17 2023 at 19:01)
data.finset.lattice mathlib4#1606 (17 messages, latest: Jan 17 2023 at 16:30)
What does "unexpected syntax" mean? (6 messages, latest: Jan 17 2023 at 15:11)
Order.SupIndep mathlib4#1627 (6 messages, latest: Jan 17 2023 at 14:29)
Abelian categories (4 messages, latest: Jan 17 2023 at 12:47)
Can't SmulCommClass.symm be an instance? (6 messages, latest: Jan 17 2023 at 11:44)
data.real.basic mathlib4#1514 (44 messages, latest: Jan 17 2023 at 08:59)
Help with Universe Levels (18 messages, latest: Jan 17 2023 at 03:29)
Transparency setting in solve_by_elim (9 messages, latest: Jan 17 2023 at 01:48)
Finset.Prod: ambigiuous notation (6 messages, latest: Jan 16 2023 at 21:10)
rw seeing through type synonym? (52 messages, latest: Jan 16 2023 at 20:31)
A translate tactic (72 messages, latest: Jan 16 2023 at 18:56)
#1594 Order.Grade (2 messages, latest: Jan 16 2023 at 17:34)
Algebra.Order.Hom.Ring #1482 (1 message, latest: Jan 16 2023 at 17:04)
Definition of subset (20 messages, latest: Jan 16 2023 at 11:18)
list.repeat (30 messages, latest: Jan 16 2023 at 10:48)
Algebra.Hom.GroupAction mathlib4#1424 (2 messages, latest: Jan 16 2023 at 10:45)
Sep notation (6 messages, latest: Jan 16 2023 at 10:15)
Int division, again (1 message, latest: Jan 16 2023 at 10:10)
How to import a file in test/ in another file in test/? (2 messages, latest: Jan 16 2023 at 09:12)
List (2 messages, latest: Jan 16 2023 at 09:08)
Data.Finset.Basic mathlib4#1555 (37 messages, latest: Jan 16 2023 at 08:03)
IsTrans (33 messages, latest: Jan 15 2023 at 21:16)
=> notation (146 messages, latest: Jan 15 2023 at 18:48)
Algebra.Free (8 messages, latest: Jan 15 2023 at 16:22)
simp only does decidable checks? (8 messages, latest: Jan 15 2023 at 10:10)
BEq DecidableEq Diamond (22 messages, latest: Jan 15 2023 at 06:37)
Notes on Ordmap.Ordnode (8 messages, latest: Jan 15 2023 at 04:04)
what's the n argument for Repr.reprPrec? (3 messages, latest: Jan 15 2023 at 00:37)
Correct formulation of induction principles (24 messages, latest: Jan 15 2023 at 00:00)
Rat in norm_num (97 messages, latest: Jan 14 2023 at 22:32)
Question about implicit coercions and the linter (8 messages, latest: Jan 14 2023 at 22:07)
✔ false alarm about norm_num (11 messages, latest: Jan 14 2023 at 21:14)
Randomness (89 messages, latest: Jan 14 2023 at 20:00)
rw not working as expected (9 messages, latest: Jan 14 2023 at 17:42)
Algebra.Hom.GroupAction (19 messages, latest: Jan 14 2023 at 14:28)
Mathport $ -> <\| (11 messages, latest: Jan 14 2023 at 13:48)
docs4 broken (5 messages, latest: Jan 14 2023 at 13:39)
simpNF definition of "simplified"? (25 messages, latest: Jan 14 2023 at 10:37)
semi/irreducible attributes (14 messages, latest: Jan 14 2023 at 09:41)
unexpected eliminator resulting type (6 messages, latest: Jan 14 2023 at 08:42)
Some Smuls in code (3 messages, latest: Jan 14 2023 at 06:58)
Similar theorems in different files with same name (5 messages, latest: Jan 14 2023 at 05:49)
defLemma failing when it seems it shouldn't (5 messages, latest: Jan 14 2023 at 04:59)
mathport fails after mathlib4 update (9 messages, latest: Jan 14 2023 at 03:58)
casesm / constructorm on no match: error or not? (10 messages, latest: Jan 13 2023 at 23:48)
"help wanted" (3 messages, latest: Jan 13 2023 at 23:23)
mathport import naming (2 messages, latest: Jan 13 2023 at 22:06)
Possible to remove rename_i here? (2 messages, latest: Jan 13 2023 at 21:17)
Test for dsimp vs simp with simp lint? (12 messages, latest: Jan 13 2023 at 19:50)
naming conventions (231 messages, latest: Jan 13 2023 at 18:46)
docs4#Rat.den_nz (1 message, latest: Jan 13 2023 at 18:08)
Data.Set.Semiring (21 messages, latest: Jan 13 2023 at 16:49)
data.int.succ_pred (3 messages, latest: Jan 13 2023 at 15:38)
simpNF (5 messages, latest: Jan 13 2023 at 15:36)
trans attribute (19 messages, latest: Jan 13 2023 at 14:57)
Order.Hom.Bounded mathlib4#888 (2 messages, latest: Jan 13 2023 at 14:37)
tt/ff (6 messages, latest: Jan 13 2023 at 14:33)
updating names in VSCode (3 messages, latest: Jan 13 2023 at 13:30)
structured CLI apps (1 message, latest: Jan 13 2023 at 11:50)
general JSON to lean4 support (7 messages, latest: Jan 13 2023 at 11:15)
Data.Multiset.Basic mathlib4#1491 (64 messages, latest: Jan 13 2023 at 09:39)
Eq.recOn (8 messages, latest: Jan 13 2023 at 08:55)
missing Decidable instances (8 messages, latest: Jan 13 2023 at 08:44)
Data.List.Sublists mathlib4#1494 (16 messages, latest: Jan 13 2023 at 08:37)
Data.Fin.Basic (mathlib4#1084) (255 messages, latest: Jan 13 2023 at 06:56)
print instances (1 message, latest: Jan 13 2023 at 03:49)
moving Data.List.Perm to std (1 message, latest: Jan 12 2023 at 23:41)
split syntax (2 messages, latest: Jan 12 2023 at 23:08)
norm_cast bug (9 messages, latest: Jan 12 2023 at 22:17)
SetTheory.Game.Pgame (3 messages, latest: Jan 12 2023 at 21:54)
interval_oc naming scheme (10 messages, latest: Jan 12 2023 at 21:03)
Order.Circular mathlib4#1489 (38 messages, latest: Jan 12 2023 at 18:45)
#align (16 messages, latest: Jan 12 2023 at 18:37)
Data.List.Sublists (1 message, latest: Jan 12 2023 at 17:53)
to_additive can't map multiplicative ℕ to ℕ (5 messages, latest: Jan 12 2023 at 11:57)
Heterogeneous scalar multiplication (26 messages, latest: Jan 12 2023 at 11:29)
application type mismatch error (2 messages, latest: Jan 12 2023 at 09:44)
lean bump (5 messages, latest: Jan 12 2023 at 08:56)
help wanted porting Algebra.Hom.Centroid (16 messages, latest: Jan 12 2023 at 08:32)
port Data.Set.Intervals.Instances (7 messages, latest: Jan 12 2023 at 08:10)
elaborate eliminator (2 messages, latest: Jan 12 2023 at 07:10)
Data.List.Rotate mathlib#1490 (3 messages, latest: Jan 12 2023 at 04:32)
Invertible 1 simps (37 messages, latest: Jan 12 2023 at 02:23)
Parsing error (7 messages, latest: Jan 12 2023 at 00:41)
List.Mem as Or? (3 messages, latest: Jan 11 2023 at 20:30)
Universes issue in mathlib#1464 (3 messages, latest: Jan 11 2023 at 20:18)
mathport runs (20 messages, latest: Jan 11 2023 at 19:42)
Data.List.Perm mathlib4#1478 (19 messages, latest: Jan 11 2023 at 16:35)
List.union (50 messages, latest: Jan 11 2023 at 13:23)
Data.List.Intervals mathlib4#1479 (1 message, latest: Jan 11 2023 at 08:01)
Data.List.Perm (6 messages, latest: Jan 11 2023 at 04:45)
typeclass instance problem with singleton (15 messages, latest: Jan 11 2023 at 03:52)
apply function to hypothesis (9 messages, latest: Jan 11 2023 at 02:47)
Array (55 messages, latest: Jan 11 2023 at 01:27)
premature "goals accomplished" (92 messages, latest: Jan 11 2023 at 00:46)
rw failing to rewrite coercions…but only sometimes (27 messages, latest: Jan 10 2023 at 20:59)
Data.List.Range mathlib4#1463 (3 messages, latest: Jan 10 2023 at 20:47)
ext (34 messages, latest: Jan 10 2023 at 19:59)
What's the general fix for Lean too eagerly unfolding (1 message, latest: Jan 10 2023 at 18:58)
Data.List.Nodup (mathlib4#1456) (2 messages, latest: Jan 10 2023 at 17:27)
Data.Set.Pointwise.Basic (mathlib4#1188) (8 messages, latest: Jan 10 2023 at 16:33)
rewrite tactic reaching maximum heartbeat (3 messages, latest: Jan 10 2023 at 15:42)
renaming in mathport (1 message, latest: Jan 10 2023 at 13:36)
Control.Traversable.Instances (mathlib4#1393) (1 message, latest: Jan 10 2023 at 12:03)
Data.List.Count (mathlib4#1410) (11 messages, latest: Jan 10 2023 at 12:01)
mathport funext (19 messages, latest: Jan 10 2023 at 10:09)
Data.List.Func (15 messages, latest: Jan 10 2023 at 09:45)
coe type linter (1 message, latest: Jan 10 2023 at 07:10)
Get-cache (57 messages, latest: Jan 10 2023 at 06:00)
local attribute [- …] (125 messages, latest: Jan 09 2023 at 21:40)
dangerous instances (2 messages, latest: Jan 09 2023 at 20:50)
Data.List.BigOperators.Basic mathlib4#1380 (12 messages, latest: Jan 09 2023 at 19:19)
improved interaction of to_additive with other attributes (4 messages, latest: Jan 09 2023 at 18:38)
Identity map of Natural Numbers is strictly monotone (3 messages, latest: Jan 09 2023 at 08:49)
rename Nat.le_or_eq_or_le_succ (2 messages, latest: Jan 09 2023 at 04:46)
Rat.floor (6 messages, latest: Jan 08 2023 at 17:44)
norm_cast (15 messages, latest: Jan 08 2023 at 17:41)
two errors (15 messages, latest: Jan 08 2023 at 17:28)
rfl (4 messages, latest: Jan 08 2023 at 13:33)
Nat.mod 0 n = 0 no longer true by rfl (32 messages, latest: Jan 08 2023 at 12:14)
data.nat.bitwise (57 messages, latest: Jan 08 2023 at 03:37)
Linarith with nats (10 messages, latest: Jan 07 2023 at 23:50)
simp experts: priority for commutatitve case? (20 messages, latest: Jan 07 2023 at 20:42)
spelling Bool-valued operations (12 messages, latest: Jan 07 2023 at 18:01)
map_natCast (3 messages, latest: Jan 07 2023 at 17:11)
Functor id / Seq id (4 messages, latest: Jan 07 2023 at 17:02)
positivity (1 message, latest: Jan 07 2023 at 16:50)
Proving if rhs is some a lhs must be some (21 messages, latest: Jan 07 2023 at 09:43)
✔ simp normal form (1 message, latest: Jan 07 2023 at 08:45)
Starting a project with Mathlib4 dependency fails… (22 messages, latest: Jan 07 2023 at 08:12)
Writing tests that fail (22 messages, latest: Jan 07 2023 at 08:01)
SimpNF failing to suggest right simp (2 messages, latest: Jan 07 2023 at 07:52)
making pr in mathlib4 (12 messages, latest: Jan 07 2023 at 06:09)
source header (19 messages, latest: Jan 07 2023 at 05:09)
Try this (6 messages, latest: Jan 07 2023 at 04:18)
Interaction of abel with casting (12 messages, latest: Jan 07 2023 at 03:18)
naming: map_int_cast vs map_natCast vs map_ratCast (18 messages, latest: Jan 07 2023 at 03:13)
Data.Real.CauSeq (mathlib4#1124) (12 messages, latest: Jan 07 2023 at 03:12)
Non-local behaviour in abel (24 messages, latest: Jan 07 2023 at 01:00)
Importing Data.String.Basic (25 messages, latest: Jan 07 2023 at 00:41)
lake update (8 messages, latest: Jan 06 2023 at 18:47)
Github actions (6 messages, latest: Jan 06 2023 at 17:51)
to_isSomePropStructure (7 messages, latest: Jan 06 2023 at 17:45)
ad hoc files (2 messages, latest: Jan 06 2023 at 15:25)
docs4#Int.ofNat_le (3 messages, latest: Jan 06 2023 at 14:46)
# The following files have been modified since … (42 messages, latest: Jan 06 2023 at 14:41)
Mass edit tools (8 messages, latest: Jan 06 2023 at 12:37)
Merging mathlib3 PRs before creating forward-ports (25 messages, latest: Jan 06 2023 at 10:21)
Last sorries in mathlib4 (16 messages, latest: Jan 06 2023 at 09:51)
resetI (9 messages, latest: Jan 06 2023 at 09:13)
deprecated.group (13 messages, latest: Jan 06 2023 at 07:57)
toDual/ofDual alignment (5 messages, latest: Jan 06 2023 at 05:44)
mfld_set_tac broken (5 messages, latest: Jan 06 2023 at 05:31)
✔ linarith failure (2 messages, latest: Jan 06 2023 at 01:34)
Issue porting Algebra.Hom.Centroid.coe_to_add_monoid_hom… (13 messages, latest: Jan 06 2023 at 00:08)
typeclass instance that fails linting (13 messages, latest: Jan 05 2023 at 23:50)
Porting Nat.mod_def (11 messages, latest: Jan 05 2023 at 23:48)
see commits in deleted branch? (15 messages, latest: Jan 05 2023 at 22:42)
porting requests (117 messages, latest: Jan 05 2023 at 22:26)
Data.Fin.Basic (41 messages, latest: Jan 05 2023 at 22:02)
Data.List.Basic (223 messages, latest: Jan 05 2023 at 21:57)
Monad List (12 messages, latest: Jan 05 2023 at 19:54)
ambiguous interpretation at Data.List.Infix (15 messages, latest: Jan 05 2023 at 19:47)
bugs and issues in the Data.List.Infix port (4 messages, latest: Jan 05 2023 at 19:12)
unsafe def (5 messages, latest: Jan 05 2023 at 18:53)
simp can prove it (46 messages, latest: Jan 05 2023 at 17:53)
New PRs (125 messages, latest: Jan 05 2023 at 16:56)
Coercion to function dificulty (28 messages, latest: Jan 05 2023 at 14:45)
simp? drops ← (1 message, latest: Jan 05 2023 at 14:23)
pinned dependencies (19 messages, latest: Jan 05 2023 at 13:48)
docs4#Set.BijOn (3 messages, latest: Jan 05 2023 at 12:28)
docs#int.nat_mod (18 messages, latest: Jan 05 2023 at 11:56)
merging or squash merging? (10 messages, latest: Jan 05 2023 at 10:26)
Data.Rat.MetaDefs (6 messages, latest: Jan 05 2023 at 09:41)
simp? trace (1 message, latest: Jan 05 2023 at 09:32)
simp normal form (52 messages, latest: Jan 04 2023 at 22:29)
problems installing lean4/mathlib4 (1 message, latest: Jan 04 2023 at 20:43)
strange error in to_additive (5 messages, latest: Jan 04 2023 at 17:29)
port_status not picking up a PR (15 messages, latest: Jan 04 2023 at 09:30)
Scoped attribute (10 messages, latest: Jan 04 2023 at 07:46)
mathport and forward-porting (21 messages, latest: Jan 04 2023 at 01:56)
✔ How does one avoid rename_i here? (4 messages, latest: Jan 04 2023 at 01:55)
How does one avoid rename_i here? (1 message, latest: Jan 04 2023 at 01:28)
mathport lag (9 messages, latest: Jan 04 2023 at 00:59)
syntax/macro question (5 messages, latest: Jan 03 2023 at 19:22)
elab_strategy (13 messages, latest: Jan 03 2023 at 17:19)
✔ some_spec (4 messages, latest: Jan 03 2023 at 10:48)
Nat.lt_add_left (2 messages, latest: Jan 03 2023 at 10:38)
dependent PRs (21 messages, latest: Jan 03 2023 at 10:05)
mathlib4 dark theme (2 messages, latest: Jan 03 2023 at 08:38)
✔ coe and norm_cast (7 messages, latest: Jan 02 2023 at 21:45)
Performance issue with CompleteBooleanAlgebra (57 messages, latest: Jan 02 2023 at 20:58)
synchronization label bot (28 messages, latest: Jan 02 2023 at 20:51)
Exists elaboration and bUnion (17 messages, latest: Jan 02 2023 at 19:50)
Kleisli(Cat) (15 messages, latest: Jan 02 2023 at 18:05)
Order.SuccPred.Relation (5 messages, latest: Jan 02 2023 at 13:51)
porting Data.Nat.WithBot (8 messages, latest: Jan 02 2023 at 12:44)
unknown attributes (11 messages, latest: Jan 02 2023 at 08:16)
Data.Int.Bitwise mathlib4#1159 (2 messages, latest: Jan 02 2023 at 07:53)
Bug in rcases? (2 messages, latest: Jan 02 2023 at 05:29)
(2 : ℕ+) (16 messages, latest: Jan 01 2023 at 23:47)
obviously replacement in category theory (6 messages, latest: Jan 01 2023 at 23:36)
Local notation conflict (9 messages, latest: Jan 01 2023 at 20:51)
export (1 message, latest: Jan 01 2023 at 19:21)
nat.bit / nat.binary_rec (21 messages, latest: Jan 01 2023 at 18:37)
version incompatibilities (4 messages, latest: Dec 31 2022 at 21:18)
Modeq name (74 messages, latest: Dec 31 2022 at 15:21)
data.rat.cast mathlib4#1261 (3 messages, latest: Dec 31 2022 at 04:54)
complete partial order formalization (9 messages, latest: Dec 30 2022 at 13:18)
mathport simps translation (1 message, latest: Dec 29 2022 at 11:16)
#queue4 (9 messages, latest: Dec 29 2022 at 11:10)
algebra.euclidean_domain.instances (6 messages, latest: Dec 28 2022 at 19:47)
(deleted) (1 message, latest: Dec 28 2022 at 18:46)
porting Data.RBTree.Init (9 messages, latest: Dec 28 2022 at 15:29)
Docs navigation (6 messages, latest: Dec 27 2022 at 21:00)
Name check (5 messages, latest: Dec 27 2022 at 20:17)
Subtype.mono_coe (2 messages, latest: Dec 27 2022 at 18:36)
How to spell coe in Lean4 (4 messages, latest: Dec 27 2022 at 16:56)
by exact (1 message, latest: Dec 27 2022 at 13:53)
aesop (31 messages, latest: Dec 27 2022 at 12:19)
ordcontinuous (8 messages, latest: Dec 27 2022 at 11:25)
instance names (12 messages, latest: Dec 27 2022 at 05:42)
typeclass loops (4 messages, latest: Dec 27 2022 at 00:12)
SimpNF issues in PNat.find (5 messages, latest: Dec 26 2022 at 21:35)
TC synthesis timeout (9 messages, latest: Dec 26 2022 at 19:58)
Data.Real.CauSeq (107 messages, latest: Dec 26 2022 at 16:36)
Data.Vector3 (10 messages, latest: Dec 26 2022 at 14:06)
pretty printing Equiv (17 messages, latest: Dec 26 2022 at 11:21)
[mathlib/test/.lean](topic/mathlib.2Ftest.2F.2Elean.html) (3 messages, latest: Dec 25 2022 at 20:47)
Name for ZFC Set (12 messages, latest: Dec 25 2022 at 19:50)
<| (20 messages, latest: Dec 25 2022 at 17:55)
Porting Dlist.lean (12 messages, latest: Dec 25 2022 at 15:57)
docBlame (44 messages, latest: Dec 25 2022 at 01:29)
simp not using a simp lemma (18 messages, latest: Dec 24 2022 at 19:38)
More issues with normalization to pp'able equalities (3 messages, latest: Dec 24 2022 at 19:16)
ci on master is failing (2 messages, latest: Dec 24 2022 at 19:05)
simp discharging (5 messages, latest: Dec 24 2022 at 17:07)
Mathlib.Order.Copy (8 messages, latest: Dec 24 2022 at 15:35)
attribute [local simp] (5 messages, latest: Dec 24 2022 at 13:31)
github permission (37 messages, latest: Dec 24 2022 at 13:24)
ₓ (6 messages, latest: Dec 24 2022 at 13:03)
#align to_additive (3 messages, latest: Dec 24 2022 at 11:08)
alias & #align (1 message, latest: Dec 24 2022 at 10:06)
git error from port_status on macOS (43 messages, latest: Dec 24 2022 at 00:17)
Data.Int.Associated (3 messages, latest: Dec 24 2022 at 00:03)
Control.Fix (2 messages, latest: Dec 23 2022 at 23:17)
Data.Set.Pairwise (40 messages, latest: Dec 23 2022 at 19:41)
Docs not updated (44 messages, latest: Dec 23 2022 at 19:03)
Mathlib.Order.ConditionallyCompleteLattice.Basic (21 messages, latest: Dec 23 2022 at 18:07)
LawfulMonad (4 messages, latest: Dec 23 2022 at 17:22)
Data.Rat.Lemmas mathlib4#1138 (1 message, latest: Dec 23 2022 at 13:55)
Classical.choose (2 messages, latest: Dec 23 2022 at 06:53)
lift (6 messages, latest: Dec 22 2022 at 22:02)
rcases (36 messages, latest: Dec 22 2022 at 21:09)
use (51 messages, latest: Dec 22 2022 at 20:16)
Data.Nat.EvenOddRec (99 messages, latest: Dec 22 2022 at 19:59)
data.nat.prime #1156 (18 messages, latest: Dec 22 2022 at 16:49)
local linting in porting wiki? (3 messages, latest: Dec 22 2022 at 14:30)
pow_succ (8 messages, latest: Dec 22 2022 at 14:02)
Order.Hom.Order mathlib4#1152 (4 messages, latest: Dec 22 2022 at 12:16)
deriving instances (5 messages, latest: Dec 22 2022 at 08:34)
div notation and rfl (13 messages, latest: Dec 22 2022 at 01:21)
square roots are square roots (35 messages, latest: Dec 22 2022 at 00:41)
Lean not "seeing through" composition (29 messages, latest: Dec 22 2022 at 00:08)
dsimp before rw (24 messages, latest: Dec 21 2022 at 23:25)
simp only [foo] not working but simp [foo] works (9 messages, latest: Dec 21 2022 at 20:26)
naming convention check (2 messages, latest: Dec 21 2022 at 19:46)
Data.Set.Lattice (13 messages, latest: Dec 21 2022 at 19:33)
Algebra.Ring.Pi (12 messages, latest: Dec 21 2022 at 18:30)
Algebra.Ring.Equiv help request (23 messages, latest: Dec 21 2022 at 17:58)
complete_lattice and has_sup (43 messages, latest: Dec 21 2022 at 15:42)
mathport ∀ a b c ∈ s (13 messages, latest: Dec 21 2022 at 13:41)
mathlib4#1129 (39 messages, latest: Dec 21 2022 at 02:16)
data.nat.bits (148 messages, latest: Dec 20 2022 at 22:39)
Data.Int.Gcd - NormNum (9 messages, latest: Dec 20 2022 at 17:36)
✔ porting autoparams with identifiers (2 messages, latest: Dec 20 2022 at 17:35)
diffing porting PR against initial commit (11 messages, latest: Dec 20 2022 at 15:39)
port status (59 messages, latest: Dec 20 2022 at 13:59)
CategoryTheory.Functor.FullyFaithful (62 messages, latest: Dec 20 2022 at 08:55)
Data.Rat.Defs (128 messages, latest: Dec 20 2022 at 02:03)
to_additive interaction with reducible (3 messages, latest: Dec 20 2022 at 00:06)
Why is coe_mk no longer needed? (8 messages, latest: Dec 19 2022 at 23:57)
porting autoparams with identifiers (1 message, latest: Dec 19 2022 at 22:46)
mathlib4-port-status-new (12 messages, latest: Dec 19 2022 at 21:54)
Set.compl and HasCompl.compl (5 messages, latest: Dec 19 2022 at 20:01)
leanproject port command (18 messages, latest: Dec 19 2022 at 19:15)
refine_struct alternative? (5 messages, latest: Dec 19 2022 at 18:15)
Order.GaloisConnection (43 messages, latest: Dec 19 2022 at 16:48)
Naming clarification (92 messages, latest: Dec 19 2022 at 16:08)
Alignment not firing (7 messages, latest: Dec 19 2022 at 12:53)
import Lean (5 messages, latest: Dec 19 2022 at 10:34)
Algebra.GroupPower.Lemmas (40 messages, latest: Dec 19 2022 at 10:11)
make MulOpposite a structure (15 messages, latest: Dec 18 2022 at 22:47)
where did the noisy linter go? (7 messages, latest: Dec 18 2022 at 20:07)
HasInvolutiveReverse / HasReverse (1 message, latest: Dec 18 2022 at 10:14)
What is 2? (8 messages, latest: Dec 18 2022 at 10:02)
Pi.Single misnomer (6 messages, latest: Dec 17 2022 at 22:45)
✔ Porting long strings after to_additive? (6 messages, latest: Dec 17 2022 at 21:26)
Porting long strings after to_additive? (1 message, latest: Dec 17 2022 at 21:02)
norm_cast: badly shaped lemma (31 messages, latest: Dec 17 2022 at 19:24)
doc blame linter and prop (4 messages, latest: Dec 17 2022 at 18:50)
notation3 (31 messages, latest: Dec 17 2022 at 18:48)
to_additive questions and issues (64 messages, latest: Dec 17 2022 at 11:09)
Problems with variables being unused (4 messages, latest: Dec 17 2022 at 06:51)
Dealing with HMul (etc.)? (3 messages, latest: Dec 17 2022 at 00:45)
not porting pi_instance (14 messages, latest: Dec 16 2022 at 22:57)
unexpected variables (10 messages, latest: Dec 16 2022 at 21:46)
Int.coe_natAbs misnomer (19 messages, latest: Dec 16 2022 at 17:40)
data.set.intervals.basic (23 messages, latest: Dec 16 2022 at 16:13)
Online docs (17 messages, latest: Dec 16 2022 at 11:49)
Porting Data.String.Basic (15 messages, latest: Dec 16 2022 at 09:45)
scoped[NS] (25 messages, latest: Dec 16 2022 at 08:11)
Syntax for unpacking structures (39 messages, latest: Dec 16 2022 at 00:01)
Nasty order of arguments dependency for @[refl] (7 messages, latest: Dec 15 2022 at 23:55)
Order.Bounded mathlib4#1042 (3 messages, latest: Dec 15 2022 at 21:24)
bors batch info (2 messages, latest: Dec 15 2022 at 19:37)
alias unfolds definitions (8 messages, latest: Dec 15 2022 at 17:56)
Logic.Equiv.Set (2 messages, latest: Dec 15 2022 at 17:14)
Algebra.Group.Opposite (18 messages, latest: Dec 15 2022 at 16:27)
Algebra.GroupPower.Order (16 messages, latest: Dec 15 2022 at 13:34)
Difference in simp behaviour (62 messages, latest: Dec 15 2022 at 11:08)
Data.Set.Enumerate (8 messages, latest: Dec 15 2022 at 09:21)
data.set.function (25 messages, latest: Dec 15 2022 at 08:36)
source references (1 message, latest: Dec 15 2022 at 08:09)
cases assumption name (4 messages, latest: Dec 15 2022 at 03:01)
CI: Cancelling outdated builds (5 messages, latest: Dec 15 2022 at 02:37)
✔ error building mathlib4 (6 messages, latest: Dec 15 2022 at 00:41)
✔ use prebuilt release? (4 messages, latest: Dec 14 2022 at 23:57)
merging (9 messages, latest: Dec 14 2022 at 23:47)
fixing library_note references (5 messages, latest: Dec 14 2022 at 20:55)
unique term inhabiting the unit (13 messages, latest: Dec 14 2022 at 20:13)
unfold working differently in Lean 4 (4 messages, latest: Dec 14 2022 at 19:59)
#1001 failed to synthesize instance (7 messages, latest: Dec 14 2022 at 18:11)
Heuristics for "typeclass instance problem"? (2 messages, latest: Dec 14 2022 at 17:37)
simpNF and MulOpposite (3 messages, latest: Dec 14 2022 at 17:24)
mathport issues in data.int.least_greatest (15 messages, latest: Dec 14 2022 at 16:54)
existential binding (9 messages, latest: Dec 14 2022 at 10:41)
Data.Part (5 messages, latest: Dec 14 2022 at 09:30)
data.int.gcd (9 messages, latest: Dec 14 2022 at 09:07)
Data.Int.Order.Basic (23 messages, latest: Dec 14 2022 at 08:09)
failed to synthesize instance Applicative id (11 messages, latest: Dec 14 2022 at 02:36)
simp regression with MonoidHomClass (11 messages, latest: Dec 14 2022 at 00:56)
#align when mathport has it right (9 messages, latest: Dec 13 2022 at 23:34)
✔ using mathlib4 tactics in porting? (4 messages, latest: Dec 13 2022 at 23:14)
assert_not_exists (1 message, latest: Dec 13 2022 at 21:40)
bool.tt (9 messages, latest: Dec 13 2022 at 18:14)
✔ split fails but constructor works. (3 messages, latest: Dec 13 2022 at 18:02)
split fails but constructor works. (5 messages, latest: Dec 13 2022 at 16:15)
referring to namespace in theorem name (3 messages, latest: Dec 13 2022 at 16:13)
indentation issue in mathport (2 messages, latest: Dec 13 2022 at 14:18)
implicit argument in mathlibport field (5 messages, latest: Dec 13 2022 at 13:56)
Int.ofNat and Nat.Cast (36 messages, latest: Dec 13 2022 at 11:43)
Structure inheritance (2 messages, latest: Dec 12 2022 at 15:10)
@[simps] making lemmas not in simp normal form (14 messages, latest: Dec 12 2022 at 10:32)
Type synonyms (81 messages, latest: Dec 12 2022 at 09:59)
div_def (4 messages, latest: Dec 12 2022 at 08:36)
FunLike issues (60 messages, latest: Dec 12 2022 at 08:00)
data.set.image (6 messages, latest: Dec 12 2022 at 07:12)
data.set.basic (164 messages, latest: Dec 12 2022 at 06:51)
Exists and simp_rw (5 messages, latest: Dec 11 2022 at 23:24)
to_additive failure (9 messages, latest: Dec 11 2022 at 19:21)
#align and simps (3 messages, latest: Dec 11 2022 at 19:12)
Porting category theory (28 messages, latest: Dec 10 2022 at 17:18)
#port-status not showing modified files (52 messages, latest: Dec 09 2022 at 19:23)
Emitting warnings in mathlib3 CI (8 messages, latest: Dec 09 2022 at 18:59)
set image notation (34 messages, latest: Dec 09 2022 at 14:22)
simp (or refl?) difference Lean 3/4 (33 messages, latest: Dec 09 2022 at 13:58)
Difference in simp lemma priorities? (11 messages, latest: Dec 09 2022 at 13:56)
simp failing on partial application of projections (7 messages, latest: Dec 09 2022 at 12:21)
simp calls broken in mathlib4#922 (17 messages, latest: Dec 09 2022 at 12:21)
bors crashed (6 messages, latest: Dec 09 2022 at 11:01)
add_pow (5 messages, latest: Dec 09 2022 at 08:47)
local semireducible (12 messages, latest: Dec 09 2022 at 04:03)
expected '}' error from mathport (10 messages, latest: Dec 08 2022 at 22:33)
request for help (7 messages, latest: Dec 08 2022 at 20:30)
OfNat (60 messages, latest: Dec 08 2022 at 18:37)
topology.algebra.order.basic (11 messages, latest: Dec 08 2022 at 15:43)
elaboration failure in algebra.order.group.units (3 messages, latest: Dec 08 2022 at 12:07)
Relying on instance names (27 messages, latest: Dec 08 2022 at 07:59)
mathport #print (18 messages, latest: Dec 07 2022 at 22:54)
#align and to_additive (12 messages, latest: Dec 07 2022 at 02:15)
coe_mk and similar lemmas (8 messages, latest: Dec 06 2022 at 23:50)
data.typevec (7 messages, latest: Dec 06 2022 at 23:36)
coe_fn vs CoeFun (3 messages, latest: Dec 06 2022 at 22:57)
unusedHavesSuffices false positive (7 messages, latest: Dec 06 2022 at 22:38)
✔ algebra.order.group.defs mathlib4#869 (2 messages, latest: Dec 06 2022 at 22:05)
when does mathlib3port run / running it myself (6 messages, latest: Dec 06 2022 at 22:04)
Naming smul vs sMul (7 messages, latest: Dec 06 2022 at 21:49)
WriterT type variation on port (7 messages, latest: Dec 06 2022 at 18:38)
algebra.order.group.defs mathlib4#869 (2 messages, latest: Dec 06 2022 at 12:32)
Auto-implicits (36 messages, latest: Dec 06 2022 at 11:44)
attributes in docs (6 messages, latest: Dec 06 2022 at 10:21)
file not in the list (4 messages, latest: Dec 06 2022 at 10:01)
typeclass timeout (27 messages, latest: Dec 06 2022 at 07:57)
symm attribute failure (13 messages, latest: Dec 06 2022 at 04:32)
status of data.nat.bits (10 messages, latest: Dec 06 2022 at 03:30)
parsing ⇑ (8 messages, latest: Dec 06 2022 at 01:11)
symm (7 messages, latest: Dec 05 2022 at 23:33)
list.traverse (27 messages, latest: Dec 05 2022 at 20:10)
Porting Algebra.Group.Ext (31 messages, latest: Dec 05 2022 at 13:53)
Searching a DiscrTree (2 messages, latest: Dec 05 2022 at 11:47)
mul_equiv.Pi_congr_right_refl (6 messages, latest: Dec 05 2022 at 09:45)
to_additive and #align (11 messages, latest: Dec 05 2022 at 00:04)
to_additive and coe (20 messages, latest: Dec 04 2022 at 22:25)
data.real.basic (12 messages, latest: Dec 04 2022 at 17:51)
plan for data.json? (8 messages, latest: Dec 04 2022 at 16:05)
data.list.defs mathlib4#803 (3 messages, latest: Dec 04 2022 at 16:02)
Pretty-printing binary operations (19 messages, latest: Dec 04 2022 at 15:59)
mapM' (12 messages, latest: Dec 04 2022 at 11:02)
by { } (30 messages, latest: Dec 04 2022 at 10:37)
Functor.map name collision (16 messages, latest: Dec 04 2022 at 01:56)
(Has)InvolutiveInv (9 messages, latest: Dec 04 2022 at 01:35)
_proof_1 (2 messages, latest: Dec 04 2022 at 01:29)
mathlib4#838 (3 messages, latest: Dec 03 2022 at 20:26)
refine vs refine' (14 messages, latest: Dec 03 2022 at 18:53)
monotoneOn_univ (4 messages, latest: Dec 03 2022 at 17:15)
message in mathlib3port file (23 messages, latest: Dec 03 2022 at 17:04)
porting instructions: runLinter? (1 message, latest: Dec 03 2022 at 14:40)
lean3port (17 messages, latest: Dec 03 2022 at 14:36)
Algebra.Ring.Basic (25 messages, latest: Dec 03 2022 at 13:59)
intermediate versions (11 messages, latest: Dec 03 2022 at 00:22)
algebra.group.with_one (11 messages, latest: Dec 02 2022 at 23:46)
instance loop? (39 messages, latest: Dec 02 2022 at 23:21)
Status of data.list.defs? (48 messages, latest: Dec 02 2022 at 22:19)
Semigroup.to_isAssociative (9 messages, latest: Dec 02 2022 at 20:51)
Field notation and CoeFun (28 messages, latest: Dec 02 2022 at 20:28)
lean_core.data.vector (4 messages, latest: Dec 02 2022 at 19:28)
Porting CategoryTheory.NaturalIso (11 messages, latest: Dec 02 2022 at 17:45)
modified since verified (46 messages, latest: Dec 02 2022 at 11:34)
mathlib4#665 - Data.Stream.Defs (11 messages, latest: Dec 02 2022 at 10:07)
Path Sequences (18 messages, latest: Dec 02 2022 at 07:56)
Missing Lean 4 defs (12 messages, latest: Dec 01 2022 at 21:09)
how to configure jump to definition (11 messages, latest: Dec 01 2022 at 20:52)
Failure to synthesize instance (11 messages, latest: Dec 01 2022 at 17:54)
how does one get a higher_order annotation in Lean 4? (4 messages, latest: Dec 01 2022 at 16:12)
Applicative variants of Monadic functions (4 messages, latest: Dec 01 2022 at 15:58)
why dubious? (8 messages, latest: Dec 01 2022 at 07:52)
List.head (14 messages, latest: Dec 01 2022 at 05:08)
zify broken? (6 messages, latest: Dec 01 2022 at 02:52)
Algebra.Field.Defs mathlib4#668 (12 messages, latest: Nov 30 2022 at 23:55)
commit convention (13 messages, latest: Nov 30 2022 at 18:11)
mathport/align questions (5 messages, latest: Nov 30 2022 at 17:51)
Sigma types or Parameters? (7 messages, latest: Nov 30 2022 at 16:05)
control_laws_tac (3 messages, latest: Nov 30 2022 at 13:17)
computability (3 messages, latest: Nov 30 2022 at 09:39)
data.nat.basic mathlib4#729 (1 message, latest: Nov 30 2022 at 08:11)
ac_refl (6 messages, latest: Nov 30 2022 at 03:28)
mathlib4#793 (3 messages, latest: Nov 30 2022 at 02:40)
ext.1 (5 messages, latest: Nov 30 2022 at 00:15)
data.nat.basic mathlib3#729 (3 messages, latest: Nov 30 2022 at 00:05)
multiple environment changing attributes (8 messages, latest: Nov 30 2022 at 00:00)
MonadRun (5 messages, latest: Nov 29 2022 at 23:47)
congrArg or congr_arg (5 messages, latest: Nov 29 2022 at 22:45)
min and max in LinearOrder (2 messages, latest: Nov 29 2022 at 21:25)
submodules (59 messages, latest: Nov 29 2022 at 20:55)
Pretty printing of existential quantifier broken (11 messages, latest: Nov 29 2022 at 20:51)
What to port? (15 messages, latest: Nov 29 2022 at 20:35)
simp (17 messages, latest: Nov 29 2022 at 19:48)
category theory (1 message, latest: Nov 29 2022 at 19:27)
mathlib4#659 Algebra.Hom.Group (12 messages, latest: Nov 29 2022 at 19:18)
Prod.Lex vs Lex (6 messages, latest: Nov 29 2022 at 18:05)
instance search sees through type synonyms (4 messages, latest: Nov 29 2022 at 17:53)
Std4 vs Mathlib4 (5 messages, latest: Nov 29 2022 at 16:56)
xor for Bool (9 messages, latest: Nov 29 2022 at 16:49)
style of multiple if let expressions (12 messages, latest: Nov 29 2022 at 15:54)
fatal: ambiguous argument 'mathlib4#771..HEAD' (5 messages, latest: Nov 29 2022 at 07:58)
porting has_reflected and friends (15 messages, latest: Nov 28 2022 at 22:36)
✔ OrderTop.ext_top (7 messages, latest: Nov 28 2022 at 22:30)
type synonym trickery not working (20 messages, latest: Nov 28 2022 at 21:00)
requesting help on mathlib4#674 (24 messages, latest: Nov 28 2022 at 17:00)
leanproject errors with import-graph, etc (5 messages, latest: Nov 28 2022 at 16:38)
OrderTop.ext_top (5 messages, latest: Nov 28 2022 at 13:51)
to_additive instance priority (11 messages, latest: Nov 28 2022 at 13:19)
✔ More to_additive issues (10 messages, latest: Nov 28 2022 at 11:09)
ENnReal (61 messages, latest: Nov 28 2022 at 09:07)
mathlib#17733 (8 messages, latest: Nov 28 2022 at 09:05)
Subtype.val not a coe (54 messages, latest: Nov 28 2022 at 03:24)
More to_additive issues (4 messages, latest: Nov 28 2022 at 01:37)
Implicit arguments in definition of subset (8 messages, latest: Nov 27 2022 at 22:08)
splitting order.bounded_order (8 messages, latest: Nov 27 2022 at 19:58)
withMainContext (7 messages, latest: Nov 27 2022 at 07:34)
Coe, CoeHead, CoeTail (18 messages, latest: Nov 27 2022 at 04:54)
FAQ on porting (22 messages, latest: Nov 27 2022 at 03:33)
non defeq in mathlib4#735 (6 messages, latest: Nov 26 2022 at 22:23)
naming ext lemmas (2 messages, latest: Nov 26 2022 at 20:10)
Naming for forall/exists as theorem names (9 messages, latest: Nov 26 2022 at 18:33)
proof review in mathlib4#728 (14 messages, latest: Nov 26 2022 at 18:26)
default files (33 messages, latest: Nov 26 2022 at 16:44)
✔ github access (2 messages, latest: Nov 25 2022 at 22:09)
github access (4 messages, latest: Nov 25 2022 at 21:55)
Nat.find (1 message, latest: Nov 25 2022 at 19:55)
mysterious error related to outParam (1 message, latest: Nov 25 2022 at 19:51)
list.nth_le (7 messages, latest: Nov 25 2022 at 08:21)
Defanging the unnecessary seqFocus linter (4 messages, latest: Nov 24 2022 at 23:23)
List-like interface for String? (7 messages, latest: Nov 24 2022 at 22:21)
GroupWithZero extends (2 messages, latest: Nov 24 2022 at 20:07)
Nudge porting move_add (1 message, latest: Nov 24 2022 at 18:27)
Can someone explain what's going on here? (15 messages, latest: Nov 24 2022 at 17:58)
instances are no longer protected (9 messages, latest: Nov 24 2022 at 17:55)
Logic for ULift lemmas (2 messages, latest: Nov 24 2022 at 15:08)
to_additive issues (56 messages, latest: Nov 24 2022 at 08:06)
Prop-valued field names (33 messages, latest: Nov 24 2022 at 06:59)
Naming for prop valued structure fields (2 messages, latest: Nov 24 2022 at 03:52)
to_additive and iffs with Exists (21 messages, latest: Nov 24 2022 at 01:53)
data.set.finite (40 messages, latest: Nov 24 2022 at 00:13)
Naming & notation: Algebra.Order.AbsoluteValue (4 messages, latest: Nov 23 2022 at 22:18)
editing PRs (1 message, latest: Nov 23 2022 at 20:33)
logic.equiv.basic mathlib4#631 (53 messages, latest: Nov 23 2022 at 19:09)
Procedure for using add_port_comments.py (4 messages, latest: Nov 23 2022 at 19:00)
Set notation (6 messages, latest: Nov 23 2022 at 17:55)
algebra.order.field.power missing (21 messages, latest: Nov 23 2022 at 17:48)
merge powers (1 message, latest: Nov 23 2022 at 13:35)
PR #15691 (1 message, latest: Nov 23 2022 at 10:55)
↑1 = 1? (10 messages, latest: Nov 23 2022 at 10:54)
✔ Dependency between branches on mathlib4 (4 messages, latest: Nov 22 2022 at 21:39)
11-20 nightly mathlib3port (15 messages, latest: Nov 22 2022 at 20:05)
to_additive and instances (11 messages, latest: Nov 22 2022 at 14:06)
LibrarySearch application type mismatch (Nat + Subsingleton) (16 messages, latest: Nov 22 2022 at 04:36)
mathlib4#588 (10 messages, latest: Nov 22 2022 at 00:02)
mathlib4#549 (3 messages, latest: Nov 21 2022 at 23:47)
What does simpa using foo do? (34 messages, latest: Nov 21 2022 at 21:14)
recursive definitions in instance fields (22 messages, latest: Nov 21 2022 at 19:44)
to_additive thinks it's in a namespace (3 messages, latest: Nov 21 2022 at 09:42)
import-graph lookahead (9 messages, latest: Nov 21 2022 at 08:50)
debug simp max recursion depth reached (3 messages, latest: Nov 21 2022 at 03:44)
What files were ported in #641? (22 messages, latest: Nov 21 2022 at 02:54)
old_structure_cmd (13 messages, latest: Nov 21 2022 at 00:33)
Instance search for nat pow times out (4 messages, latest: Nov 20 2022 at 23:20)
Status of Algebra.Group.Commute? (2 messages, latest: Nov 20 2022 at 21:30)
checking that mathbin and mathlib port capture decls (6 messages, latest: Nov 20 2022 at 21:09)
porting tool assistance (7 messages, latest: Nov 20 2022 at 19:22)
1+1 = 2 (10 messages, latest: Nov 20 2022 at 14:03)
data.stream.defs (6 messages, latest: Nov 20 2022 at 12:14)
add_port_comments.py (11 messages, latest: Nov 20 2022 at 12:06)
mathlib4#655 (10 messages, latest: Nov 20 2022 at 09:38)
help with a failing to_additive (26 messages, latest: Nov 20 2022 at 09:23)
Linting standards for mathlib (23 messages, latest: Nov 20 2022 at 08:28)
Universe lint & Ulift (21 messages, latest: Nov 20 2022 at 07:11)
pi_instance(_derive_field): possible changes? (9 messages, latest: Nov 20 2022 at 02:13)
EmbeddingLike (10 messages, latest: Nov 20 2022 at 01:18)
Do port status scripts belong in mathlibtools or mathlib? (9 messages, latest: Nov 20 2022 at 00:33)
algebra.hierarchy_design (7 messages, latest: Nov 19 2022 at 23:13)
✔ "Theory development" VS "tactic porting" (3 messages, latest: Nov 19 2022 at 19:12)
max_default/min_default (8 messages, latest: Nov 19 2022 at 10:07)
logic.equiv.basic (23 messages, latest: Nov 19 2022 at 08:22)
porting lazylist (7 messages, latest: Nov 19 2022 at 07:35)
invalid occurrence of universe level (14 messages, latest: Nov 19 2022 at 02:39)
Attribute pp_nodot (3 messages, latest: Nov 19 2022 at 01:35)
Should we mark Mathlib.Data.RBTree.* as ported? (7 messages, latest: Nov 19 2022 at 01:33)
multifile PRs (3 messages, latest: Nov 19 2022 at 00:37)
How to clone mathlib4 (17 messages, latest: Nov 18 2022 at 22:20)
Option.get (5 messages, latest: Nov 18 2022 at 22:04)
solve two goals with [tac1,tac2] (2 messages, latest: Nov 18 2022 at 22:04)
Documentation on lint overrides? (5 messages, latest: Nov 18 2022 at 21:56)
default proofs (17 messages, latest: Nov 18 2022 at 21:54)
align tag (4 messages, latest: Nov 18 2022 at 21:26)
capitals in Logic.Equiv.Defs file (13 messages, latest: Nov 18 2022 at 21:15)
double-capital identifiers (9 messages, latest: Nov 18 2022 at 20:57)
congr attribute (7 messages, latest: Nov 18 2022 at 20:10)
porting Algebra/Quotient (9 messages, latest: Nov 18 2022 at 12:39)
Porting monads (23 messages, latest: Nov 18 2022 at 10:59)
simp on Compares downstream effects (5 messages, latest: Nov 18 2022 at 03:12)
Docstring style? (4 messages, latest: Nov 18 2022 at 00:52)
mathlib4#560 (14 messages, latest: Nov 18 2022 at 00:36)
logic.equiv.defs mathlib4#550 (3 messages, latest: Nov 18 2022 at 00:22)
good first port – good beginner files (11 messages, latest: Nov 17 2022 at 23:57)
CI for checking files are imported (5 messages, latest: Nov 17 2022 at 23:01)
printing inferInstance (4 messages, latest: Nov 17 2022 at 22:45)
Linting in VS code (14 messages, latest: Nov 17 2022 at 22:41)
data.nat.cast.defs (17 messages, latest: Nov 17 2022 at 20:34)
protecting structure projections (3 messages, latest: Nov 17 2022 at 19:41)
dsimp and simp (5 messages, latest: Nov 17 2022 at 19:39)
porting localized (42 messages, latest: Nov 17 2022 at 19:37)
data.sigma.default (20 messages, latest: Nov 17 2022 at 19:01)
vscode with remote repositories failing to find toolchain (5 messages, latest: Nov 17 2022 at 13:53)
to_additive and noncomputable (2 messages, latest: Nov 17 2022 at 13:42)
Local notation (8 messages, latest: Nov 17 2022 at 13:37)
mathlib4#604 (3 messages, latest: Nov 17 2022 at 11:33)
Zulip shortcuts (9 messages, latest: Nov 17 2022 at 07:03)
How to help (9 messages, latest: Nov 17 2022 at 05:43)
zify (34 messages, latest: Nov 17 2022 at 05:08)
missing tactic port (37 messages, latest: Nov 17 2022 at 03:57)
auto_param.check_exists in ported file (4 messages, latest: Nov 17 2022 at 00:44)
Catalog of porting patterns? (4 messages, latest: Nov 16 2022 at 17:03)
Check that all files are imported (8 messages, latest: Nov 16 2022 at 15:18)
#align in namespaces (4 messages, latest: Nov 16 2022 at 11:57)
capitalisation and dot notation (5 messages, latest: Nov 16 2022 at 11:23)
Linting (15 messages, latest: Nov 16 2022 at 10:40)
fixing easy error in Mathbin (4 messages, latest: Nov 16 2022 at 10:35)
by_cases spacing (2 messages, latest: Nov 16 2022 at 10:14)
has_seq vs Seq (2 messages, latest: Nov 16 2022 at 07:57)
Should mllist be MLList (6 messages, latest: Nov 16 2022 at 05:07)
verifying ported files against mathlib (25 messages, latest: Nov 16 2022 at 04:45)
How to find instances (11 messages, latest: Nov 15 2022 at 20:43)
has_reflect (14 messages, latest: Nov 15 2022 at 20:28)
aligns without content? (4 messages, latest: Nov 15 2022 at 20:17)
style guide (2 messages, latest: Nov 15 2022 at 19:39)
simp timeing out (15 messages, latest: Nov 15 2022 at 05:56)
some useful automation (73 messages, latest: Nov 15 2022 at 04:01)
Basic porting questions (6 messages, latest: Nov 14 2022 at 20:53)
using eta-rfl for Equiv (16 messages, latest: Nov 14 2022 at 15:01)
logic.equiv.defs causing elaboration issues in Simps tests (4 messages, latest: Nov 14 2022 at 08:08)
"Ported by:" docstring (5 messages, latest: Nov 13 2022 at 16:26)
protecting master (1 message, latest: Nov 13 2022 at 06:36)
best way to help? (27 messages, latest: Nov 13 2022 at 05:43)
linear order on Int (3 messages, latest: Nov 11 2022 at 12:55)
simp! does not unfold abbrevs (2 messages, latest: Nov 11 2022 at 04:17)
congr_arg not unifying HMul (3 messages, latest: Nov 11 2022 at 04:07)
rw side goal proofs (7 messages, latest: Nov 11 2022 at 04:04)
simpNF error "unknown metavariable" (10 messages, latest: Nov 11 2022 at 03:57)
Omitting indexing type in a pi type (6 messages, latest: Nov 11 2022 at 00:45)
to_additive (2 messages, latest: Nov 10 2022 at 13:32)
Updating mathlib3port (22 messages, latest: Nov 09 2022 at 17:39)
∃ {n : ℕ} (14 messages, latest: Nov 09 2022 at 15:59)
eqv_gen (6 messages, latest: Nov 09 2022 at 15:20)
indentation (6 messages, latest: Nov 09 2022 at 13:49)
mathlib4#557 (15 messages, latest: Nov 09 2022 at 07:02)
root (5 messages, latest: Nov 08 2022 at 23:04)
min/max definitions non-alignment (20 messages, latest: Nov 08 2022 at 09:37)
Using inferInstance as partial fills in instance defs (18 messages, latest: Nov 08 2022 at 04:36)
Equality of structures with autoparams (15 messages, latest: Nov 07 2022 at 19:12)
to_additive on structures (4 messages, latest: Nov 07 2022 at 04:34)
align for Repr.reprPrec (3 messages, latest: Nov 07 2022 at 04:15)
LinearOrder in mathlib3/4 (14 messages, latest: Nov 07 2022 at 03:42)
to_additive interaction with strings and syntax highlight (4 messages, latest: Nov 07 2022 at 03:25)
mathlib4#537 (2 messages, latest: Nov 06 2022 at 08:42)
norm_num for non-semirings (9 messages, latest: Nov 05 2022 at 20:27)
equivalence relations are symmetric (7 messages, latest: Nov 05 2022 at 12:25)
attribute [instance, priority 10] coe_fn_trans (4 messages, latest: Nov 05 2022 at 04:54)
include/omit (3 messages, latest: Nov 05 2022 at 03:39)
mathlib 3 ready to merge PR (3 messages, latest: Nov 05 2022 at 02:59)
[RFC] refine_struct functionality via new ?.. syntax (1 message, latest: Nov 04 2022 at 02:08)
refine_struct (4 messages, latest: Nov 03 2022 at 22:23)
convert_to (20 messages, latest: Nov 01 2022 at 23:39)
zify mathlib4#517 (3 messages, latest: Oct 31 2022 at 05:22)
need help placating simpNF linter (45 messages, latest: Oct 30 2022 at 15:08)
#align bug when already aligned (2 messages, latest: Oct 30 2022 at 14:28)
Porting status for lean3 core (12 messages, latest: Oct 30 2022 at 07:05)
Importing a file changed dite if macro semantics (7 messages, latest: Oct 30 2022 at 04:45)
how to include mathlib4 in the lakefile? (6 messages, latest: Oct 28 2022 at 22:58)
mathlib4#511 (4 messages, latest: Oct 28 2022 at 22:29)
✔ invalid simp theorem (2 messages, latest: Oct 28 2022 at 18:20)
invalid simp theorem (3 messages, latest: Oct 28 2022 at 18:18)
List and monads (4 messages, latest: Oct 27 2022 at 09:16)
Move some tactics to separate package? (8 messages, latest: Oct 27 2022 at 01:08)
Injective (15 messages, latest: Oct 25 2022 at 00:46)
xor (2 messages, latest: Oct 24 2022 at 21:19)
and_self (5 messages, latest: Oct 24 2022 at 21:09)
error while loading shared libraries (2 messages, latest: Oct 24 2022 at 20:35)
to_additive and smul (4 messages, latest: Oct 24 2022 at 11:15)
tooling (1 message, latest: Oct 24 2022 at 10:30)
unusedArguments linter not referencing nolints (6 messages, latest: Oct 24 2022 at 05:42)
Should boolean or_assoc be a simp lemma? (10 messages, latest: Oct 24 2022 at 03:26)
local notation for subtypes (4 messages, latest: Oct 23 2022 at 23:37)
porting core Lean 3 stuff? (9 messages, latest: Oct 23 2022 at 22:12)
lean 3/4 bool ! precedence (3 messages, latest: Oct 21 2022 at 20:53)
porting logic.basic (54 messages, latest: Oct 21 2022 at 10:42)
toBool (23 messages, latest: Oct 21 2022 at 08:25)
data.option.defs (6 messages, latest: Oct 21 2022 at 07:35)
porting algebra.order.ring_lemmas (5 messages, latest: Oct 20 2022 at 18:32)
[t1, …, tn] combinator (5 messages, latest: Oct 20 2022 at 10:26)
dropping import Mathbin support (1 message, latest: Oct 20 2022 at 04:45)
Exists.some_spec alignment seems to not be working (6 messages, latest: Oct 20 2022 at 04:08)
proposal for marking files as frozen (115 messages, latest: Oct 20 2022 at 01:14)
to_additive and multiple parents (3 messages, latest: Oct 20 2022 at 00:34)
error when executing port status script (6 messages, latest: Oct 19 2022 at 22:43)
porting data.bool.basic (3 messages, latest: Oct 19 2022 at 19:47)
importing binported oleans (1 message, latest: Oct 19 2022 at 18:33)
porting data.sigma.basic (29 messages, latest: Oct 19 2022 at 12:05)
linting (2 messages, latest: Oct 18 2022 at 20:42)
empty type (8 messages, latest: Oct 18 2022 at 18:21)
porting questions (9 messages, latest: Oct 18 2022 at 17:11)
ring failure (2 messages, latest: Oct 18 2022 at 16:31)
is_refl (25 messages, latest: Oct 18 2022 at 00:06)
Understanding tauto.lean (mathlib3) (60 messages, latest: Oct 17 2022 at 23:33)
problem with change (18 messages, latest: Oct 17 2022 at 18:31)
missing attributes (6 messages, latest: Oct 17 2022 at 07:23)
Using QQ when you only have an Expr (6 messages, latest: Oct 17 2022 at 03:11)
Some naming questions (15 messages, latest: Oct 16 2022 at 22:00)
data.prod (3 messages, latest: Oct 16 2022 at 20:24)
status of ring (9 messages, latest: Oct 14 2022 at 10:32)
elaborate context in attributes (15 messages, latest: Oct 13 2022 at 21:02)
porting names (7 messages, latest: Oct 11 2022 at 14:22)
A QQ about Nat (4 messages, latest: Oct 11 2022 at 04:37)
weirdness with ofNat (3 messages, latest: Oct 11 2022 at 04:15)
Changed API for SatisfiesM_mapIdxM.go (2 messages, latest: Oct 10 2022 at 21:00)
by_contra when goal is an implication (6 messages, latest: Oct 10 2022 at 20:41)
#457 (40 messages, latest: Oct 10 2022 at 03:31)
Which files to port? (203 messages, latest: Oct 08 2022 at 04:52)
solve_aux (9 messages, latest: Oct 06 2022 at 04:32)
DecidableEq vs BEq and LawfulHashable (5 messages, latest: Oct 04 2022 at 17:20)
rfl tactic (42 messages, latest: Sep 29 2022 at 18:29)
using binport only (136 messages, latest: Sep 28 2022 at 20:17)
using mathlib3port (7 messages, latest: Sep 24 2022 at 02:52)
mathlib4 vs std4 (3 messages, latest: Sep 22 2022 at 18:00)
wlog #16495 (4 messages, latest: Sep 21 2022 at 06:59)
difficulty porting List.perm_inv_core (10 messages, latest: Sep 19 2022 at 04:57)
rfl tactic (1 message, latest: Sep 18 2022 at 21:22)
guardHyp (14 messages, latest: Sep 18 2022 at 20:48)
choose (48 messages, latest: Sep 17 2022 at 14:47)
dsimp conv (16 messages, latest: Sep 16 2022 at 18:17)
Deprecated defs (5 messages, latest: Sep 16 2022 at 03:39)
Exists Unique (2 messages, latest: Sep 13 2022 at 10:20)
wlog (10 messages, latest: Sep 13 2022 at 08:47)
✔ existsi (3 messages, latest: Sep 09 2022 at 17:07)
trying to run mathport (30 messages, latest: Sep 09 2022 at 13:29)
cc (6 messages, latest: Sep 08 2022 at 15:47)
mapply (2 messages, latest: Sep 06 2022 at 05:43)
Building mathlib 4 (1 message, latest: Sep 02 2022 at 05:07)
status of binport syntax (5 messages, latest: Aug 31 2022 at 13:49)
Changing instance priority (14 messages, latest: Aug 07 2022 at 02:28)
Do we still have plenty of time before the port? (4 messages, latest: Aug 03 2022 at 16:36)
Mathlib/Lean/ vs Mathlib/Util/ (5 messages, latest: Jul 27 2022 at 01:33)
mathlib4#342 (1 message, latest: Jul 23 2022 at 22:03)
Tensor product of bounded operators (3 messages, latest: Jul 22 2022 at 18:46)
mathport: cases_on => casesOn (30 messages, latest: Jun 30 2022 at 19:38)
porting progress (23 messages, latest: Jun 28 2022 at 12:37)
mathlib4 priorities (22 messages, latest: Jun 27 2022 at 17:58)
mathport improvements for data.num.add (14 messages, latest: Jun 27 2022 at 16:25)
How to install mathlib4 (16 messages, latest: Jun 27 2022 at 09:50)
✔ can't import tactic (1 message, latest: May 23 2022 at 13:39)
can't import tactic (5 messages, latest: May 23 2022 at 13:03)
Porting streams (Nat → α) (10 messages, latest: May 20 2022 at 13:12)
push_neg behavior (10 messages, latest: May 10 2022 at 13:34)
✔ left and right tactics (1 message, latest: May 03 2022 at 15:54)
left and right tactics (2 messages, latest: May 03 2022 at 12:46)
✔ autoImplicit confusion? (1 message, latest: Apr 29 2022 at 09:26)
autoImplicit confusion? (3 messages, latest: Apr 29 2022 at 02:13)
(interactive) conv mode (25 messages, latest: Apr 28 2022 at 11:44)
mathlib newbie issue: exists tactic (10 messages, latest: Apr 25 2022 at 23:55)
Fixing rcases for nightly (8 messages, latest: Apr 20 2022 at 08:24)
Symm and Trans tactics implementation (2 messages, latest: Apr 06 2022 at 05:26)
lean core nightly bump (6 messages, latest: Apr 05 2022 at 16:37)
Symm tactic implementation (13 messages, latest: Apr 05 2022 at 11:14)
Propagate Tags (10 messages, latest: Apr 05 2022 at 00:48)
Syntax triage (13 messages, latest: Apr 04 2022 at 14:11)
Proof of false using library_search (12 messages, latest: Apr 03 2022 at 02:35)
set tactic and elab benefits? (25 messages, latest: Mar 23 2022 at 18:43)
✔ congr tactic: first steps (8 messages, latest: Mar 23 2022 at 07:41)
congr tactic: first steps (76 messages, latest: Mar 23 2022 at 06:52)
Push_neg port (4 messages, latest: Mar 21 2022 at 07:55)
expand have capabilities (162 messages, latest: Mar 18 2022 at 23:56)
replace tactic (23 messages, latest: Mar 17 2022 at 18:18)
Installation demo (8 messages, latest: Mar 17 2022 at 13:39)
port unfold_wf (1 message, latest: Mar 16 2022 at 20:06)
prioritizing porting efforts (18 messages, latest: Mar 16 2022 at 09:15)
✔ simpa tactic (1 message, latest: Mar 15 2022 at 20:40)
is restate_axiom needed? (8 messages, latest: Mar 15 2022 at 19:23)
squeeze_simp and simp? (38 messages, latest: Mar 15 2022 at 18:30)
stream events (10 messages, latest: Mar 14 2022 at 20:01)
simpa tactic (32 messages, latest: Mar 14 2022 at 19:16)
getting started with joining the porting effort (9 messages, latest: Mar 14 2022 at 10:11)
State of mathlib4? (4 messages, latest: Mar 12 2022 at 18:49)
work_on_goal vs swap (68 messages, latest: Mar 04 2022 at 12:12)
Tactic status? (169 messages, latest: Mar 01 2022 at 13:30)
independent and auxiliary (10 messages, latest: Feb 21 2022 at 21:41)
adding to std (20 messages, latest: Feb 20 2022 at 13:50)
mathlib4 as a dependency? (11 messages, latest: Feb 19 2022 at 20:27)
Q. about ByteSlice.getOp (29 messages, latest: Feb 11 2022 at 05:33)
rotate (119 messages, latest: Feb 07 2022 at 15:31)
tests that expect failure (3 messages, latest: Feb 06 2022 at 19:25)
swap semantics tactics names (44 messages, latest: Feb 05 2022 at 01:23)
swap semantics (32 messages, latest: Feb 04 2022 at 19:06)
Tatic equivalent (4 messages, latest: Feb 03 2022 at 17:28)
mathlib3port as a dependency (8 messages, latest: Jan 28 2022 at 16:19)
Ring tactic bug? (8 messages, latest: Jan 25 2022 at 23:10)
✔ When mathlib4 (5 messages, latest: Jan 23 2022 at 20:47)
When mathlib4 (5 messages, latest: Jan 22 2022 at 23:06)
import data.nat (4 messages, latest: Jan 11 2022 at 16:19)
Aggressiveness of nat literal conversion (6 messages, latest: Jan 11 2022 at 07:50)
Explicit/implicit argument of Inhabited.default (12 messages, latest: Jan 07 2022 at 14:36)
is mathlib made only by the community? (5 messages, latest: Jan 06 2022 at 02:00)
Ordered merge slower than append-then-sort (22 messages, latest: Jan 02 2022 at 18:02)
✔ New Project that uses MathLib4 (5 messages, latest: Dec 26 2021 at 11:09)
porting record (1 message, latest: Dec 23 2021 at 07:51)
Mathport abs syntax clash (21 messages, latest: Dec 14 2021 at 18:07)
generating Mathlib.lean (6 messages, latest: Dec 14 2021 at 05:24)
More issues with OfNat (42 messages, latest: Dec 14 2021 at 02:45)
Signed integers (13 messages, latest: Dec 13 2021 at 21:42)
Deterministic timeout with Inhabited from Zero (14 messages, latest: Dec 13 2021 at 10:38)
porting simps and to_additive (99 messages, latest: Dec 09 2021 at 21:48)
comments (19 messages, latest: Nov 29 2021 at 10:47)
Renaming split (92 messages, latest: Nov 29 2021 at 04:12)
Referencing mathlib 4 from module (7 messages, latest: Nov 14 2021 at 00:44)
mathport re-org (6 messages, latest: Nov 11 2021 at 23:39)
getting mathlib running (16 messages, latest: Nov 08 2021 at 21:06)
decide vs Decidable.to_bool (9 messages, latest: Oct 30 2021 at 00:11)
International docs (10 messages, latest: Oct 27 2021 at 21:27)
add import Leanbin.Init.Default in synported files (106 messages, latest: Oct 20 2021 at 09:20)
0🔶 ("zero diamond") (11 messages, latest: Oct 18 2021 at 17:53)
✔ "Use" tactic implementation in lean 4 (12 messages, latest: Oct 18 2021 at 16:42)
"Use" tactic implementation in lean 4 (7 messages, latest: Oct 18 2021 at 07:45)
PR to use lake (1 message, latest: Oct 18 2021 at 00:14)
Update lean? (31 messages, latest: Oct 06 2021 at 02:31)
Coend calculus in Lean (1 message, latest: Oct 01 2021 at 22:06)
mathport depending on mathlib (163 messages, latest: Oct 01 2021 at 00:43)
Porting Nat/Digits (11 messages, latest: Sep 29 2021 at 22:00)
List.subset weak implicit (4 messages, latest: Sep 27 2021 at 06:13)
emacs setup (1 message, latest: Sep 22 2021 at 23:12)
Documentation mistake in algebra.covariant_and_contravariant (6 messages, latest: Sep 12 2021 at 22:21)
specialize @foo x (4 messages, latest: Sep 08 2021 at 16:06)
Instance binders in exists (26 messages, latest: Sep 08 2021 at 09:04)
mathport bump (1 message, latest: Sep 08 2021 at 02:54)
OfNat/Numeric (15 messages, latest: Sep 03 2021 at 19:46)
fun with binport (25 messages, latest: Aug 31 2021 at 22:37)
backport remove cc macros (17 messages, latest: Aug 27 2021 at 14:56)
purpose of Mathlib.lean file? (24 messages, latest: Aug 25 2021 at 05:37)
file organization in mathlib4 repo (1 message, latest: Aug 24 2021 at 00:44)
Alternative MetaM (3 messages, latest: Aug 23 2021 at 05:30)
Nat.le backport (15 messages, latest: Aug 22 2021 at 15:51)
mathport clashes (1 message, latest: Aug 21 2021 at 23:42)
help wanted: strategic binport experimentation (64 messages, latest: Aug 21 2021 at 23:15)
Building binport (2 messages, latest: Aug 21 2021 at 04:02)
profiling ring (17 messages, latest: Aug 20 2021 at 02:10)
bad simp lemmas (30 messages, latest: Aug 18 2021 at 21:50)
panic while testing ring tactic (12 messages, latest: Aug 18 2021 at 10:29)
RFC: porting strategies (42 messages, latest: Aug 15 2021 at 23:44)
structure cmd (7 messages, latest: Aug 11 2021 at 17:25)
argument order of Or.elim (6 messages, latest: Aug 05 2021 at 19:37)
Mario's FMM 2021 talk (46 messages, latest: Jul 30 2021 at 18:06)
Tactic casing convention (67 messages, latest: Jul 30 2021 at 02:10)
Lean4 math library (3 messages, latest: Jul 23 2021 at 05:45)
"· tac" block notation (96 messages, latest: Jul 22 2021 at 23:44)
close branch (5 messages, latest: Jul 12 2021 at 20:25)
#8190 (4 messages, latest: Jul 04 2021 at 13:42)
Backporting strict implicits (2 messages, latest: Jul 04 2021 at 07:12)
Push access to branches? (2 messages, latest: Jul 03 2021 at 21:23)
Data/Nat/Gcd.lean (2 messages, latest: Jun 21 2021 at 02:27)
treating mathlib as a stdlib (299 messages, latest: Jun 10 2021 at 21:03)
Experiments with algebra (5 messages, latest: Jun 04 2021 at 16:21)
sorry (13 messages, latest: Jun 03 2021 at 16:52)
github diffs trick (10 messages, latest: May 23 2021 at 13:50)
Mem notation (1 message, latest: May 23 2021 at 09:42)
List.mem (9 messages, latest: May 23 2021 at 06:07)
Schemes (1 message, latest: May 22 2021 at 10:31)
algebra hierarchy (4 messages, latest: May 18 2021 at 16:43)
.vscode (2 messages, latest: May 15 2021 at 04:32)

Last updated: Jan 31 2023 at 21:29 UTC