diff --git a/prelude/base.v b/prelude/base.v index 575a0671ffc421b3c0cf5646b1842f46cb2665d7..ab142229f48a9a4310c5e9f6157f059476936d52 100644 --- a/prelude/base.v +++ b/prelude/base.v @@ -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) :=