`#test` コマンドの活用例：プロパティベーステストを役立てる

高階関数やパラメトリック多相な関数のテストであっても、期待される式をそのまま書けてとっても便利

import Plausible

instance : Monad List where
  pure := List.singleton
  bind := List.flatMap

namespace Map
  /- ## map の再帰を使う定義と、使わない定義を比較する -/

  variable {α β : Type}

  /-- do 構文による map の実装 -/
  def List.doMap (f : α → β) (xs : List α) : List β := do
    let x ← xs
    return f x

  -- テスト
  #test
    ∀ {α β : Type} (f : α → β) (xs : List α),
    List.doMap f xs = xs.map f

end Map

universe u

instance instAlternative : Alternative List.{u} where
  failure := @List.nil
  orElse l l' := List.append l (l' ())

namespace Filter

  /- ## filter の再帰を使う定義と、使わない定義を比較する -/

  variable {α : Type}

  /-- do 構文による filter の実装 -/
  def List.doFilter (p : α → Bool) (xs : List α) : List α := do
    let x ← xs
    guard <| p x
    return x

  -- テスト
  #test
    ∀ {α : Type} (p : α → Bool) (xs : List α),
    List.doFilter p xs = List.filter p xs

end Filter

Start with the #test command and Plausible import shown in the issue. Locate the relevant Lean-by-example documentation section, then verify that the property-based testing examples for List.doMap and List.doFilter work as documented. Done means the usage example is included in the appropriate documentation and both displayed tests are valid.