I am new to Coq. I noticed it was possible to define the empty set in Coq using
Inductive Empty_set : Set :=.
Is it also possible to define the function from the empty set to another general set/type ? If so how ?
1 Answers
Yes. Just use pattern matching:
Definition of_Empty_set T (x : Empty_set) : T :=
match x with end.
Related