Changes
3 changed files (+71/-38)
-
-
@@ -1,3 +1,27 @@inductive LazyList (α : Type u) | nil | cons : α → Thunk (LazyList α) → LazyList α def LazyList.map (f: α → β) : LazyList α → LazyList β | nil => nil | cons x xs => cons (f x) <| xs.get.map f def LazyList.length {α} : LazyList α → Nat | .nil => 0 | .cons a b => b.get.length + 1 @[simp] theorem LazyList.length_map {α β} (l : LazyList α) (f : α → β) : (l.map f).length = l.length := by match l with | .nil => simp [LazyList.length, LazyList.map] | .cons x xs => simp only [LazyList.length, LazyList.map, Thunk.get]; rw [LazyList.length_map] theorem not_exists_ints : ¬∃ ints : Unit → LazyList Float, ints = (fun _ => LazyList.cons 1.0 <| (ints ()).map (· + 1)) := by intro ⟨ints, h⟩ have ss := congrArg (fun f => (f ()).length) h simp [LazyList.length, Thunk.get] at ss -- Want: -- def ints := LazyList.cons 1 <| ints.map (· + 1) -- Problem: This is recursive, bad!
-
@@ -30,56 +54,46 @@-- -- #eval ints 10 -- inductive LazyList (α : Type u) -- | nil -- | cons : α → Thunk (LazyList α) → LazyList α -- deriving Inhabited -- def LazyList.take : Nat → LazyList α → List α -- | 0, _ => .nil -- | _, nil => .nil -- | n + 1, cons x xs => .cons x <| xs.get.take n -- def LazyList.map (f: α → β) : LazyList α → LazyList β -- | nil => nil -- | cons x xs => cons (f x) <| xs.get.map f -- def LazyList.zipWith (f: α → β → γ) : LazyList α → LazyList β → LazyList γ -- | nil, _ => nil -- | _, nil => nil -- | cons x xs, cons y ys => cons (f x y) <| zipWith f xs.get ys.get inductive LazyList (α : Type u) where | nil | cons : α → Thunk (LazyList α) → LazyList α def LazyList.take : Nat → LazyList α → List α | 0, _ => .nil | _, nil => .nil | n + 1, cons x xs => .cons x <| xs.get.take n def LazyList.map (f: α → β) : LazyList α → LazyList β | nil => nil | cons x xs => cons (f x) <| xs.get.map f def LazyList.zipWith (f: α → β → γ) : LazyList α → LazyList β → LazyList γ | nil, _ => nil | _, nil => nil | cons x xs, cons y ys => cons (f x y) <| zipWith f xs.get ys.get unsafe def ints := LazyList.cons 1.0 <| ints.map (· + 1) #eval ints.take 10 -- Doesn't work? -- unsafe def integrate s (c : Float) := LazyList.cons c <| LazyList.zipWith (· / ·) s ints notation s "integrate" c => LazyList.cons c <| LazyList.zipWith (· / ·) s ints -- partial def ints _ := LazyList.cons 1.0 <| (ints ()).map (· + 1) unsafe def pows := LazyList.cons 1.0 <| LazyList.zipWith (· + ·) pows pows -- #eval (ints ()).take 10 #eval pows.take 10 -- def integrate (s : Unit → LazyList Float) (c : Float) := LazyList.cons c <| LazyList.zipWith (· / ·) (s ()) (ints ()) unsafe def expSeries := expSeries integrate 1.0 -- partial def expSeries _ := integrate expSeries 1.0 #eval expSeries.take 10 -- #eval (expSeries ()).take 10 def evalAt n (s : LazyList Float) x := (s.take n).foldr (λ a acc => a + acc * x) 0 -- def evalAt n (s : LazyList Float) x := (s.take n).foldr (λ a acc => a + acc * x) 0 mutual unsafe def sine := cosine integrate 0.0 unsafe def cosine := (sine integrate -1.0).map (-·) end -- mutual -- partial def sine _ := integrate cosine 0.0 -- partial def cosine _ := (integrate sine (-1.0)).map (-·) -- end #eval sine.take 10 -- #eval (sine ()).take 10 #eval evalAt 1000 sine 2.0 #eval 2.0.sin -- #eval evalAt 1000 (sine ()) 2.0 -- #eval 2.0.sin -- inductive LazyList (α : Type u) where -- | nil
-
-
monad.lean (new)
-
@@ -0,0 +1,12 @@def mapM [Monad m] (f : α → m β) : List α → m (List β) | [] => pure [] | x :: xs => f x >>= fun hd => mapM f xs >>= fun tl => pure (hd :: tl) #eval mapM (m := Id) (· + 1) [1, 2, 3, 4, 5] #eval show IO Unit from IO.println "hello world" #reduce show IO Unit from IO.println "hello world"
-
-
native-decide.lean (new)
-
@@ -0,0 +1,7 @@example : False := by let getHeartbeats (x : Nat) : Nat := let .ok _ state := IO.mkRef x () -- ensure `x` is not eliminated let .ok val state := IO.getNumHeartbeats state val have : getHeartbeats 0 ≠ getHeartbeats (0 + 1 - 1) := by native_decide simp [getHeartbeats] at this
-