partial_fixpoint を使える型を増やすことができる

[Seasawher]

https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/partial_fixpoint_monotone.20does.20not.20add.20the.20lemma.20to.20database/with/569941985

This works

import Lean
open Lean.Order

set_option trace.Elab.Tactic.monotonicity true

def MyType : Type := sorry

def myfun : MyType → MyType := sorry

instance : PartialOrder MyType where
  rel := sorry
  rel_refl := sorry
  rel_trans := sorry
  rel_antisymm := sorry

instance : CCPO MyType where
  has_csup := sorry

@[partial_fixpoint_monotone]
theorem myfun_mono : ∀ {α} [PartialOrder α] (f : α → MyType), monotone f → monotone (fun x => myfun (f x)) := by sorry

def works' : MyType := myfun works'
partial_fixpoint