commit c5970aab23bded15dba3131f01286ec05ccadf80
Author: qwjyh <urataw421@gmail.com>
Date:   Wed Jun 5 15:49:21 2024 +0900

    init

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..bfb30ec
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+/.lake
diff --git a/Main.lean b/Main.lean
new file mode 100644
index 0000000..4bb2483
--- /dev/null
+++ b/Main.lean
@@ -0,0 +1,62 @@
+import «MonadtSample»
+
+def ret1 : Except String Nat := .ok 10
+
+def ret2 : Except String Nat := .error "message"
+
+def rets : List (Except String Nat) := [.ok 1, .ok 10, .error "problem 1", .error "problem 2", .ok 100000]
+
+def liftIO (t : ExceptT String Id α) : IO α := do
+  match t with
+  | .ok r => EStateM.Result.ok r
+  | .error s => EStateM.Result.error s
+
+instance : MonadLift (ExceptT String Id) IO where
+  monadLift := liftIO
+
+def main : IO Unit := do
+  let fmt := Std.Format.nest 5 <| ".aa gjeoi".toFormat.append ((Std.Format.align true).append ("a".toFormat.append (Std.Format.line.append "b".toFormat)))
+  IO.println fmt
+  -- let ret ← ret2
+  -- IO.println s!"ret: {ret}"
+  -- let ret ← ret1
+  -- IO.println s!"ret: {ret}"
+  try
+    let ret ← ret1
+    IO.println s!"ret1: {ret}"
+
+    for val in rets do
+      IO.println s!"ret: {val}"
+  catch e =>
+    IO.eprintln s!"Error: {e}"
+
+#eval main
+
+#print main
+
+#eval (1.2).mul 100 |>.round |>.div 100 |>.toString |>.toFormat |>.tag 10
+
+#print Task
+
+def hoge := main.asTask
+
+#check -42.0
+#eval 10. * 10^3
+#check 10^3
+#eval (10.8).toUInt64
+#check Float.ofScientific
+#eval Float.ofScientific 323 true 1
+
+namespace Float
+def sprintf_1 (x : Float) (a : Nat) : String :=
+  let sign : Bool := x > 0
+  let up := (if sign then x.toUInt64 else (-x).toUInt64) |>.toNat
+  let down := (x - up.toFloat) * (10^a).toFloat |>.round |>.toUInt64 |>.toNat
+  let sign_sign := if sign then "" else "-"
+  s!"{sign_sign}{up}.{down}"
+end Float
+
+#eval (3.14).sprintf_1 0
+#eval (3.14).sprintf_1 1
+#eval (3.14).sprintf_1 2
+
diff --git a/MonadtSample.lean b/MonadtSample.lean
new file mode 100644
index 0000000..f71405b
--- /dev/null
+++ b/MonadtSample.lean
@@ -0,0 +1,3 @@
+-- This module serves as the root of the `MonadtSample` library.
+-- Import modules here that should be built as part of the library.
+import «MonadtSample».Basic
\ No newline at end of file
diff --git a/MonadtSample/Basic.lean b/MonadtSample/Basic.lean
new file mode 100644
index 0000000..e99d3a6
--- /dev/null
+++ b/MonadtSample/Basic.lean
@@ -0,0 +1 @@
+def hello := "world"
\ No newline at end of file
diff --git a/lake-manifest.json b/lake-manifest.json
new file mode 100644
index 0000000..59b75aa
--- /dev/null
+++ b/lake-manifest.json
@@ -0,0 +1,5 @@
+{"version": 7,
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "monadt_sample",
+ "lakeDir": ".lake"}
diff --git a/lakefile.lean b/lakefile.lean
new file mode 100644
index 0000000..d429583
--- /dev/null
+++ b/lakefile.lean
@@ -0,0 +1,12 @@
+import Lake
+open Lake DSL
+
+package «monadt_sample» where
+  -- add package configuration options here
+
+lean_lib «MonadtSample» where
+  -- add library configuration options here
+
+@[default_target]
+lean_exe «monadt_sample» where
+  root := `Main
diff --git a/lean-toolchain b/lean-toolchain
new file mode 100644
index 0000000..2bf5ad0
--- /dev/null
+++ b/lean-toolchain
@@ -0,0 +1 @@
+stable