Lean 4 Playground

Examples

Literate reStructuredText (RST)

• Hello.lean
• LAMR.lean

Literate Markdown

My Learning following various books/tutorials/games

• AllTactics.lean
• Chisolm.lean
• Filters.lean
• FiniteGroup.lean
• HelloMarkdown.lean
• Hierarchies.lean
• MV.lean
• Rank.lean
• Tactics.lean
• Utils.lean

Discussions on Zulip

• Zulip/Agatha.lean
• Zulip/Arrow.lean
• Zulip/Branch.lean
• Zulip/Calc.lean
• Zulip/Cat.lean
• Zulip/Closed.lean
• Zulip/CodeAction.lean
• Zulip/CurrentModule.lean
• Zulip/EnvExInit.lean
• Zulip/EnvExt.lean
• Zulip/EvalRewriteSeq.lean
• Zulip/FiltersMWE.lean
• Zulip/Float.lean
• Zulip/Have.lean
• Zulip/Heartbeat.lean
• Zulip/Import.lean
• Zulip/Infix.lean
• Zulip/KroneckerDelta.lean
• Zulip/LFTCM2023.lean
• Zulip/Monad.lean
• Zulip/Rintro.lean
• Zulip/SlimCheck.lean
• Zulip/SmallStep.lean
• Zulip/SpellCheck.lean
• Zulip/WithLog.lean

#eval
"4.13.0-rc3"
 
Lean.versionString: String
Lean.versionString

#eval
"4.13.0"
 
Lean.versionStringCore: String
Lean.versionStringCore

#eval
"leanprover/lean4:4.13.0-rc3"
 
Lean.toolchain: String
Lean.toolchain

#eval
"leanprover/lean4"
 
Lean.origin: String
Lean.origin

#eval
"01d414ac36dc28f3e424dabd36d818873fea655c"
 
Lean.githash: String
Lean.githash