(2 : ℕ+)

Stream: mathlib4

[Chris Hughes]

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

[Jireh Loreaux]

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

[Henrik Böving]

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]

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

[Mario Carneiro]

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]

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]

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

[Henrik Böving]

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]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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

[Henrik Böving]

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

[Heather Macbeth]

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]

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

[Niels Voss]

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.