Changes
8 changed files (+2/-8)
-
-
@@ -4,11 +4,9 @@ if !(← System.FilePath.pathExists <| (← IO.currentDir) / i) thenthrow <| IO.userError s!"{i} missing!" return String.join <| (s!"<img src=\"/{·}\">") <$> s def imgs := ["lean-anime.jpg", "proglang.png", "lean-tactics.png", "purity.png", "proglangs.jpg", "imax.jpg", "switch.jpg", "bad-apple.png", "lean-hands.png", "donotlean.jpg", "lean-inside.jpg", "lean-board-game.jpg", "operator.png", "universes.png", "lean-junk.png", "worksheet.jpg", "lean-box.jpg", "lean-sign.jpg", "flt.png", "lean-phone.png", "fbip.jpg", "discrimination.png"] def imgs := ["lean-anime.jpg", "proglang.png", "lean-tactics.png", "purity.png", "proglangs.jpg", "imax.jpg", "switch.jpg", "bad-apple.png", "lean-hands.png", "donotlean.jpg", "lean-inside.jpg", "lean-board-game.jpg", "operator.png", "universes.png", "lean-junk.png", "worksheet.jpg", "lean-box.jpg", "lean-sign.jpg", "flt.png", "lean-phone.png", "fbip.jpg", "discrimination.png", "cuisine.jpg"] def dafny_imgs := ["who-would-win.jpg", "class-change.png", "flt-dafny.png"] def other_imgs := ["ProofGeneral-image.jpg", "proof-cafe.jpg", "coq.png", "coq-bunny.jpg", "coq-gun.jpg"] def main := do IO.println s!"<!DOCTYPE html>
-
@@ -18,7 +16,5 @@ <h1>LEAN FAN SITE</h1>{← f imgs} <h2>Don't use Dafny, <a href=\"https://github.com/dafny-lang/dafny/pull/6208\">it's (still) unsound!</a></h2> {← f dafny_imgs} <h2>Other proof assistants</h2> {← f other_imgs} <p><a href=\"/Main.lean\">Made using the best language ever!</a></p> <p>Not all images are mine. Please don't sue me.</p>"
-
-
ProofGeneral-image.jpg (deleted)
-
coq-bunny.jpg (deleted)
-
coq-gun.jpg (deleted)
-
coq.png (deleted)
-
cuisine.jpg (new)
-
-
@@ -2,10 +2,8 @@ <!DOCTYPE html><link rel="stylesheet" href="style.css" type="text/css"> <title>LEAN FAN SITE</title> <h1>LEAN FAN SITE</h1> <img src="/lean-anime.jpg"><img src="/proglang.png"><img src="/lean-tactics.png"><img src="/purity.png"><img src="/proglangs.jpg"><img src="/imax.jpg"><img src="/switch.jpg"><img src="/bad-apple.png"><img src="/lean-hands.png"><img src="/donotlean.jpg"><img src="/lean-inside.jpg"><img src="/lean-board-game.jpg"><img src="/operator.png"><img src="/universes.png"><img src="/lean-junk.png"><img src="/worksheet.jpg"><img src="/lean-box.jpg"><img src="/lean-sign.jpg"><img src="/flt.png"><img src="/lean-phone.png"><img src="/fbip.jpg"><img src="/discrimination.png"> <img src="/lean-anime.jpg"><img src="/proglang.png"><img src="/lean-tactics.png"><img src="/purity.png"><img src="/proglangs.jpg"><img src="/imax.jpg"><img src="/switch.jpg"><img src="/bad-apple.png"><img src="/lean-hands.png"><img src="/donotlean.jpg"><img src="/lean-inside.jpg"><img src="/lean-board-game.jpg"><img src="/operator.png"><img src="/universes.png"><img src="/lean-junk.png"><img src="/worksheet.jpg"><img src="/lean-box.jpg"><img src="/lean-sign.jpg"><img src="/flt.png"><img src="/lean-phone.png"><img src="/fbip.jpg"><img src="/discrimination.png"><img src="/cuisine.jpg"> <h2>Don't use Dafny, <a href="https://github.com/dafny-lang/dafny/pull/6208">it's (still) unsound!</a></h2> <img src="/who-would-win.jpg"><img src="/class-change.png"><img src="/flt-dafny.png"> <h2>Other proof assistants</h2> <img src="/ProofGeneral-image.jpg"><img src="/proof-cafe.jpg"><img src="/coq.png"><img src="/coq-bunny.jpg"><img src="/coq-gun.jpg"> <p><a href="/Main.lean">Made using the best language ever!</a></p> <p>Not all images are mine. Please don't sue me.</p>
-
-
proof-cafe.jpg (deleted)