Stream: Coq users

Topic: Simple question

Rafael Garcia Leiva (Jul 30 2020 at 09:09):

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.

Jonas Oberhauser (Jul 30 2020 at 12:16):

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)

Rafael Garcia Leiva (Jul 30 2020 at 12:29):

Clear! Thanks!

Last updated: Sep 23 2023 at 15:01 UTC