search

lean-ja / lean-by-example

コード例で学ぶ Lean 言語
https://lean-ja.github.io/lean-by-example/
MIT License
48 stars 7 forks source link

`constructor` が LawfulMonad を分解できなくなる #1122

Open Seasawher opened 3 hours ago

Seasawher commented 3 hours ago 
instance : LawfulMonad Option := by
  constructor <;> sorry

instance [Monad m] [LawfulMonad m] : LawfulMonad (OptionT m) := by
  /- tactic 'constructor' failed, no applicable constructor found -/
  constructor
Seasawher commented 3 hours ago

Zulip: > constructor does not work for LawfulMonad