2020-09-01から1ヶ月間の記事一覧
A. Flat CPO Definition task := forall (x y : option nat) (n : nat), x = Some n -> x = y \/ x = None -> x = y. x = y \/ x = None について場合分けするのが簡単です。x = y の場合は自明で、x = None の場合はもう一つの仮定 x = Some n と合わせると…
A. Flat CPO Definition task := forall (x y : option nat) (n : nat), x = Some n -> x = y \/ x = None -> x = y. x = y \/ x = None について場合分けするのが簡単です。x = y の場合は自明で、x = None の場合はもう一つの仮定 x = Some n と合わせると…