Random Zulip stuff

Changes

2 changed files (+28/-0)

• DocComments.lean (new)
  • @@ -0,0 +1,14 @@
    + -- This works + /-- Moo. -/ + @[inline] + def moo (a : Nat) := a + + -- This doesn't + @[inline] + /-- Moo. -/ + def moo2 (a : Nat) := a + + open scoped Classical in + /-- Moo. -/ + @[inline] + def moo3 (a : Nat) := a
• Perf.lean (new)
  • @@ -0,0 +1,14 @@
    + import Batteries + + def a : Array Nat := Array.replicate 2000000 1 + + instance : Monad Array where + bind x f := Array.flatMap f x + pure x := #[x] + map := Array.map + + set_option trace.profiler true in + #eval Array.size (return 2 * (← a)) + + set_option trace.profiler true in + #eval ((2 * ·) <$> a).size