Functions are inhabited.

08ea7c37 · Robbert Krebbers · 9365ea8b · 08ea7c37
Commit 08ea7c37 authored May 29, 2016 by Robbert Krebbers
Hide whitespace changes
Inline Side-by-side

Showing with 3 additions and 0 deletions

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

No files found.
--- a/theories/base.v
+++ b/theories/base.v
@@ -306,6 +306,9 @@ Notation "(∘)" := compose (only parsing) : C_scope.
 Notation "( f ∘)" := (compose f) (only parsing) : C_scope.
 Notation "(∘ f )" := (λ g, compose g f) (only parsing) : C_scope.

+Instance impl_inhabited {A} `{Inhabited B} : Inhabited (A → B) :=
+  populate (λ _, inhabitant).
+
 (** Ensure that [simpl] unfolds [id], [compose], and [flip] when fully
 applied. *)
 Arguments id _ _ /.