Commit 7e6955cd authored by Robbert Krebbers's avatar Robbert Krebbers

Bool is inhabited.

parent 8b197368
...@@ -136,6 +136,7 @@ Class Inhabited (A : Type) : Type := populate { inhabitant : A }. ...@@ -136,6 +136,7 @@ Class Inhabited (A : Type) : Type := populate { inhabitant : A }.
Arguments populate {_} _. Arguments populate {_} _.
Instance unit_inhabited: Inhabited unit := populate (). Instance unit_inhabited: Inhabited unit := populate ().
Instance bool_inhabated : Inhabited bool := populate true.
Instance list_inhabited {A} : Inhabited (list A) := populate []. Instance list_inhabited {A} : Inhabited (list A) := populate [].
Instance prod_inhabited {A B} (iA : Inhabited A) Instance prod_inhabited {A B} (iA : Inhabited A)
(iB : Inhabited B) : Inhabited (A * B) := (iB : Inhabited B) : Inhabited (A * B) :=
......
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