Zulip Chat Archive

Stream: mathlib4

Topic: (2 : ℕ+)


Chris Hughes (Dec 30 2022 at 17:58):

Do we have a way to write (2 : ℕ+) in mathlib4 yet?

Jireh Loreaux (Dec 30 2022 at 18:00):

Looking at the instances listed here: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#OfNat, I suspect not.

Henrik Böving (Dec 30 2022 at 18:19):

The instances list is quite outdated because std4 master and mathlib4 master have been incompatible for weeks by now and I always try to build both masters (so the build fails)

Chris Hughes (Dec 30 2022 at 18:20):

I suppose we just have to define ofNat 0 = 1 or something for PNat. Could get confusing sometimes

Mario Carneiro (Dec 30 2022 at 18:21):

that's news to me, std4 has not changed in a while and I thought there was already a mathlib4 bump PR merged for the last thing

Mario Carneiro (Dec 30 2022 at 18:22):

It looks like the last bump was for 12-23 and affected both std4 and mathlib4, so they should be up to date right now

Henrik Böving (Dec 30 2022 at 18:29):

Maybe the doc-gen error changed in between then let me try to build locally again

Henrik Böving (Dec 30 2022 at 18:56):

Ah @Mario Carneiro it did change indeed!

λ lake -Kdoc=on build Std:docs Mathlib:docs
Building Aesop.Tree.Data
error: > LEAN_PATH=././lake-packages/CMark/build/lib:././lake-packages/lake/build/lib:././lake-packages/doc-gen4/build/lib:././lake-packages/Cli/build/lib:./build/lib:././lake-packages/Qq/build/lib:././lake-packages/aesop/build/lib:././lake-packages/leanInk/build/lib:././lake-packages/Unicode/build/lib:././lake-packages/std/build/lib LD_LIBRARY_PATH=/home/nix/.elan/toolchains/leanprover--lean4---nightly-2022-12-23/lib:././lake-packages/aesop/build/lib /home/nix/.elan/toolchains/leanprover--lean4---nightly-2022-12-23/bin/lean ././lake-packages/aesop/././Aesop/Tree/Data.lean -R ././lake-packages/aesop/./. -o ././lake-packages/aesop/build/lib/Aesop/Tree/Data.olean -i ././lake-packages/aesop/build/lib/Aesop/Tree/Data.ilean -c ././lake-packages/aesop/build/ir/Aesop/Tree/Data.c
error: stdout:
././lake-packages/aesop/././Aesop/Tree/Data.lean:388:18: error: failed to synthesize instance
  Inhabited SavedState

:(

Mario Carneiro (Dec 30 2022 at 18:57):

I see https://github.com/JLimperg/aesop/pull/37 is open

Mario Carneiro (Dec 30 2022 at 18:59):

ah, mathlib4 is actually on gebner/aesop right now, we should probably figure this out cc: @Jannis Limperg

Kevin Buzzard (Dec 31 2022 at 02:10):

When I'm defining nat.pred in class with the equation compiler, in order to prove nat.succ a = nat.succ b -> a = b, I always define pred 0 to be 37, stressing that it's a junk value. Do we have to define ofNat 0? Why not let it be 37 if so?

Jannis Limperg (Dec 31 2022 at 13:17):

I've now updated Aesop to work with the latest std4.

Henrik Böving (Dec 31 2022 at 13:19):

In that case we should see new docs in ~ 4 hours

Heather Macbeth (Dec 31 2022 at 17:51):

Do we also need to update Mathlib to work with the latest Aesop? See the build failures on mathlib4#1274, mathlib4#1278, and the latest run of doc-gen4.

Notification Bot (Dec 31 2022 at 18:12):

12 messages were moved from this topic to #mathlib4 > version incompatibilities by Heather Macbeth.

Niels Voss (Jan 01 2023 at 23:47):

Sorry if I'm misunderstanding, but I thought I read in Functional Programming in Lean 4 that the ofNat type class was flexible enough to specify which natural numbers that could be converted. A version of ofNat for only positive numbers is described here.


Last updated: Dec 20 2023 at 11:08 UTC