lean: 2015 01

2015/lean/.gitignore

@@ -0,0 +1 @@
+/.lake

2015/lean/Aoc2015.lean

@@ -0,0 +1,3 @@
+-- This module serves as the root of the `Aoc2015` library.
+-- Import modules here that should be built as part of the library.
+import «Aoc2015».Basic

2015/lean/Aoc2015/Basic.lean

@@ -0,0 +1 @@
+def hello := "world"

2015/lean/Main.lean

@@ -0,0 +1,11 @@
+import «Aoc2015»
+
+def asChange : Char -> Int
+  | '(' => 1
+  | ')' => -1
+  | _   => 0
+
+def main : IO Unit := do
+  let hello <- IO.FS.readFile "../.inputs/01.txt"
+  let sum := hello |> String.toList |> List.map asChange |> List.foldl (.+.) 0
+  IO.println sum

2015/lean/README.md

@@ -0,0 +1 @@
+# aoc2015

2015/lean/lake-manifest.json

@@ -0,0 +1,5 @@
+{"version": "1.0.0",
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "aoc2015",
+ "lakeDir": ".lake"}

2015/lean/lakefile.lean

@@ -0,0 +1,12 @@
+import Lake
+open Lake DSL
+
+package «aoc2015» where
+  -- add package configuration options here
+
+lean_lib «Aoc2015» where
+  -- add library configuration options here
+
+@[default_target]
+lean_exe «aoc2015» where
+  root := `Main

2015/lean/lean-toolchain

@@ -0,0 +1 @@
+stable