I am a newcomer to the world of Coq. Can somebody explain me the difference between
Definition Desc : Set := nat -> nat.
Parameter Desc : nat -> nat.
Many thanks in advance.
in your first definition, you have Desc = nat->nat and hence (fun x => x+2) : Desc and (fun y => 3) : Desc. In the second case, you have an uninterpreted symbol Desc of type nat->nat, which might be instantiated, e.g., with Desc = (fun x => x+2)
Last updated: Sep 23 2023 at 15:01 UTC