Commit 6e9a9572 authored by Robbert Krebbers's avatar Robbert Krebbers

COFEs on nat and bool.

parent 9fd1f58e
......@@ -273,6 +273,8 @@ End discrete_cofe.
Arguments discreteC _ {_ _}.
Definition leibnizC (A : Type) : cofeT := @discreteC A equivL _.
Canonical Structure natC := leibnizC nat.
Canonical Structure boolC := leibnizC bool.
(** Later *)
Inductive later (A : Type) : Type := Later { later_car : A }.
......
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