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.18.0-rc1" 
Lean.versionString: String
Lean.versionString

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

#eval
"leanprover/lean4:4.18.0-rc1" 
Lean.toolchain: String
Lean.toolchain

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

#eval
"69a1d0485e241a494d69d3e2c98ad988f4396dcd" 
Lean.githash: String
Lean.githash