Inhabited instance for any Empty instance.

782731f6 · Jacques-Henri Jourdan · 10a74299 · 782731f6
Commit 782731f6 authored Aug 08, 2016 by Jacques-Henri Jourdan
Hide whitespace changes
Inline Side-by-side

Showing with 2 additions and 0 deletions

theories/base.v theories/base.v +2 -0

No files found.
--- a/theories/base.v
+++ b/theories/base.v
@@ -567,6 +567,8 @@ intersection [(∩)], and difference [(∖)], the singleton [{[_]}], the subset
 Class Empty A := empty: A.
 Notation "∅" := empty : C_scope.

+Instance empty_inhabited `(Empty A) : Inhabited A := populate ∅.
+
 Class Top A := top : A.
 Notation "⊤" := top : C_scope.