Skip to content
Snippets Groups Projects
Commit 4572d5c0 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Bool is inhabited.

parent 46643628
No related branches found
No related tags found
No related merge requests found
......@@ -136,6 +136,7 @@ Class Inhabited (A : Type) : Type := populate { inhabitant : A }.
Arguments populate {_} _.
Instance unit_inhabited: Inhabited unit := populate ().
Instance bool_inhabated : Inhabited bool := populate true.
Instance list_inhabited {A} : Inhabited (list A) := populate [].
Instance prod_inhabited {A B} (iA : Inhabited A)
(iB : Inhabited B) : Inhabited (A * B) :=
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment