Open Seasawher opened 7 months ago
https://lean-lang.org/functional_programming_in_lean/monads/conveniences.html#leading-dot-notation
書くとしたら induction の項目かなと思う。
https://lean-lang.org/functional_programming_in_lean/monads/conveniences.html#leading-dot-notation