Skip to content

Commit

Permalink
Update captionlong
Browse files Browse the repository at this point in the history
  • Loading branch information
Trequetrum committed Jan 20, 2024
1 parent a27deee commit 4748d2e
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Game.lean
Original file line number Diff line number Diff line change
Expand Up @@ -172,7 +172,7 @@ Warning: In most browsers, deleting cookies will also clear the local storage
/-! Information to be displayed on the servers landing page. -/
Languages "English"
CaptionShort "Lean intro to Logic"
CaptionLong "Self-contained friendly introduction to constructive logic"
CaptionLong "A mostly self-contained introduction to constructive logic using Lean. Learn how each propositional connective can be introduced and eliminated using both terms and tactics."
CoverImage "images/logic0101.png"

/-! Build the game. Show's warnings if it found a problem with your game. -/
Expand Down

0 comments on commit 4748d2e

Please sign in to comment.