1. Top
  2. i-love-lean
  3. Files
  4. Main.lean
i-love-lean

Made using the best language ever!

  1. 1
  2. 2
  3. 3
  4. 4
  5. 5
  6. 6
  7. 7
  8. 8
  9. 9
  10. 10
  11. 11
  12. 12
  13. 13
  14. 14
  15. 15
  16. 16
  17. 17
  18. 18
  19. 19
  20. 20
  21. 21
  22. 22
  23. 23
  24. 24 
def f (s : List String) : IO String := do
  for i in s do
    if !(← System.FilePath.pathExists <| (← IO.currentDir) / i) then
      throw <| 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 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>
<link rel=\"stylesheet\" href=\"style.css\" type=\"text/css\">
<title>LEAN FAN SITE</title>
<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>"