From 7e6955cdb2945e112fd1087eff64a496d1e1ceca 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.
---
theories/base.v | 1 +
1 file changed, 1 insertion(+)
diff --git a/theories/base.v b/theories/base.v
index 575a0671..ab142229 100644
--- a/theories/base.v
+++ b/theories/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