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
andinduction
(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
withinductive
(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 intest/
? (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
Smul
s 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
vssimp
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 mapmultiplicative ℕ
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 besome
(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
vsmap_natCast
vsmap_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 withreducible
(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
andHasCompl.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 butconstructor
works. (3 messages, latest: Dec 13 2022 at 18:02) split
fails butconstructor
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
(orrefl
?) 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
andmax
inLinearOrder
(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
vsLex
(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 withimport-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 acoe
(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
beMLList
(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 asimp
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 anExpr
(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
vsBEq
andLawfulHashable
(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
stream
s (Nat → α
) (10 messages, latest: May 20 2022 at 13:12) - push_neg behavior (10 messages, latest: May 10 2022 at 13:34)
- ✔
left
andright
tactics (1 message, latest: May 03 2022 at 15:54) left
andright
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
vsswap
(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