Stream: Coq users

Topic: Simple question


view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Rafael Garcia Leiva (Jul 30 2020 at 12:29):

Clear! Thanks!


Last updated: Feb 01 2023 at 13:03 UTC