init

.gitignore

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

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
+

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

MonadtSample/Basic.lean

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

lake-manifest.json

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

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

lean-toolchain

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