Commit 230f3454 authored by Robbert Krebbers's avatar Robbert Krebbers

Unit is timeless.

parent f9f87bb2
......@@ -235,6 +235,8 @@ Section unit.
Definition unit_cofe_mixin : CofeMixin unit.
Proof. by repeat split; try exists 0. Qed.
Canonical Structure unitC : cofeT := CofeT unit_cofe_mixin.
Global Instance unit_timeless (x : ()) : Timeless x.
Proof. done. Qed.
End unit.
(** Product *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment