theory Scratch imports "Main" begin

datatype 's fail = OK 's | Fail

locale l =
  fixes m :: "'message set"
begin

type_synonym icore_adv = "unit + unit"
type_synonym 'look ocore_adv = "'look option + unit"

type_synonym 'message' icore_usr = "'message' + unit"
type_synonym 'message' ocore_usr = "unit + 'message' option"

fun foo :: "icore_adv + 'message icore_usr \<Rightarrow> 'look ocore_adv + 'message ocore_usr" where
  "foo (Inl (Inl ())) = Inl (Inl None)"
| "foo (Inl (Inr ())) = Inl (Inr ())"
| "foo (Inr (Inl message)) = Inr (Inl ())"
| "foo (Inr (Inr ())) = Inr (Inr None)"

datatype 'a state
  = Initial
  | Ready 'a

term "%x. case_fail (case_state True (\<lambda>g. False)) True x"
term "\<lambda>x. case x of OK Initial \<Rightarrow> True | OK (Ready g) \<Rightarrow> False | Fail \<Rightarrow> True"

end

end