From 4572d5c0f8ea9bff7107b5c85ede54414a28e2ad Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 13 Apr 2016 14:43:02 +0200
Subject: [PATCH] Bool is inhabited.
---
prelude/base.v | 1 +
1 file changed, 1 insertion(+)
diff --git a/prelude/base.v b/prelude/base.v
index 575a0671f..ab142229f 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) :=
--
GitLab