From 81e1d5792f26b9ec0f4dc62476fe8e4d6ef86736 Mon Sep 17 00:00:00 2001 From: Maciej Jur Date: Wed, 24 Jul 2024 22:51:48 +0200 Subject: [PATCH] lean: 2015 01 --- 2015/lean/.gitignore | 1 + 2015/lean/Aoc2015.lean | 3 +++ 2015/lean/Aoc2015/Basic.lean | 1 + 2015/lean/Main.lean | 11 +++++++++++ 2015/lean/README.md | 1 + 2015/lean/lake-manifest.json | 5 +++++ 2015/lean/lakefile.lean | 12 ++++++++++++ 2015/lean/lean-toolchain | 1 + 8 files changed, 35 insertions(+) create mode 100644 2015/lean/.gitignore create mode 100644 2015/lean/Aoc2015.lean create mode 100644 2015/lean/Aoc2015/Basic.lean create mode 100644 2015/lean/Main.lean create mode 100644 2015/lean/README.md create mode 100644 2015/lean/lake-manifest.json create mode 100644 2015/lean/lakefile.lean create mode 100644 2015/lean/lean-toolchain diff --git a/2015/lean/.gitignore b/2015/lean/.gitignore new file mode 100644 index 0000000..bfb30ec --- /dev/null +++ b/2015/lean/.gitignore @@ -0,0 +1 @@ +/.lake diff --git a/2015/lean/Aoc2015.lean b/2015/lean/Aoc2015.lean new file mode 100644 index 0000000..2640b9f --- /dev/null +++ b/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 \ No newline at end of file diff --git a/2015/lean/Aoc2015/Basic.lean b/2015/lean/Aoc2015/Basic.lean new file mode 100644 index 0000000..e99d3a6 --- /dev/null +++ b/2015/lean/Aoc2015/Basic.lean @@ -0,0 +1 @@ +def hello := "world" \ No newline at end of file diff --git a/2015/lean/Main.lean b/2015/lean/Main.lean new file mode 100644 index 0000000..c46cbb5 --- /dev/null +++ b/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 diff --git a/2015/lean/README.md b/2015/lean/README.md new file mode 100644 index 0000000..4692f58 --- /dev/null +++ b/2015/lean/README.md @@ -0,0 +1 @@ +# aoc2015 \ No newline at end of file diff --git a/2015/lean/lake-manifest.json b/2015/lean/lake-manifest.json new file mode 100644 index 0000000..161976c --- /dev/null +++ b/2015/lean/lake-manifest.json @@ -0,0 +1,5 @@ +{"version": "1.0.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "aoc2015", + "lakeDir": ".lake"} diff --git a/2015/lean/lakefile.lean b/2015/lean/lakefile.lean new file mode 100644 index 0000000..fe3f514 --- /dev/null +++ b/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 diff --git a/2015/lean/lean-toolchain b/2015/lean/lean-toolchain new file mode 100644 index 0000000..2bf5ad0 --- /dev/null +++ b/2015/lean/lean-toolchain @@ -0,0 +1 @@ +stable