Hi,

I am a newcomer to the world of Coq. Can somebody explain me the difference between

Definition Desc : Set := nat -> nat.

and

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)

Clear! Thanks!

Last updated: Feb 01 2023 at 13:03 UTC