Docs

Stream: new members

[Ian Riley]

Is there a docs page for Lean 4 that has all of the theorems etc. that can be used for structured proof steps and all the tactics? I've noticed that mathlib has great documentation, but I wasn't sure if there was anything similar just for Lean 4 core.

[Henrik Böving]

https://leanprover-community.github.io/mathlib4_docs/ has docs for both core and mathlib, we don't have a tactic list or something like that right now though.

[Ian Riley]

Sweet! Thank you. So there's Init Lean Mathlib and Std. Are Init Lean and Std all default included in the Lean environment whereas Mathlib is the math library via mathlib4?

[Henrik Böving]

Init is default in Lean 4. Std used to be core but it is now in a library called std4 hosted by the same github organization as mathlib4. There might be eventual plans to integrate the default distribution with std or something but that's still in the future for now. Mathlib is indeed via matlhib4

[Ian Riley]

Gotcha. I noticed that Std has Std.Tactic which includes several tactics. I solved a proof last night using the by_cases tactic which is listed in Std.Tactic but I didn't import std4. Can I assume that several of those tactics are included in Lean by default but not all? And that there might be more tactics that are in Lean that aren't listed in Std.Tactic?

[Henrik Böving]

mathlib4 does have std4 as a dependency so if you have mathlib4 you have std4

[Ian Riley]

I don't have mathlib4 either.

[Ian Riley]

Unless it's default included by lake init.

[Henrik Böving]

no

[Henrik Böving]

https://github.com/leanprover/std4/blob/bc4c3f72b28abc028fc55ea49d827089fb7e9ef4/Std/Tactic/ByCases.lean#L16

std improves on by_cases by macro rules, i assume its in core as well

[Ian Riley]

It looks like it is. I've been scanning through the Lean4 repo (which I probably should have gone to before to look for tactics). It has the byCases tactic, and I'm guessing that by_cases is just an alias for byCases.