`Prop` is inhabited.

718ca5be · Robbert Krebbers · b5a66ffb · 718ca5be
Commit 718ca5be authored Feb 14, 2020 by Robbert Krebbers
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
@@ -413,6 +413,8 @@ Class TotalOrder {A} (R : relation A) : Prop := {
 }.

 (** * Logic *)
+Instance prop_inhabited : Inhabited Prop := populate True.
+
 Notation "(∧)" := and (only parsing) : stdpp_scope.
 Notation "( A ∧.)" := (and A) (only parsing) : stdpp_scope.
 Notation "(.∧ B )" := (λ A, A ∧ B) (only parsing) : stdpp_scope.