blob: d3d5d3e5b4ba21d89618c3ea777a3fece1bc6435 (
plain)
1
2
3
4
5
6
7
8
9
10
|
Generalizable All Variables.
Class Inhabited (A : Type) : Type := populate { inhabitant : A }.
Arguments populate {_} _.
Set Mangle Names.
Axioms _0 _1 _2 : Prop.
Instance impl_inhabited {A} {B} {_3:Inhabited B} : Inhabited (A -> B)
:= populate (fun _ => inhabitant).
|
