Assignment 06_05

[alkaza]

When I solve

Inductive all {X : Type} (P : X -> Prop) : list X -> Prop 

in my MoreLogic.v file, everything works perfectly, but when I go through it in the Assignment file, it gives me an error message:

Error:
In environment
all : forall X : Type, (X -> Prop) -> list X -> Prop
X : Type
P : X -> Prop
The term "X" has type "Type" while it is expected to have type "X -> Prop".

Could you help me to figure out why does this happen?

Since the assignment says "[all X P l] asserts that [P] is true for every element of the list [l]" I assume it implies my solution...

[jaewooklee93]

I guess their difference is {X:Type} and (X:Type).

(* MoreLogic.v *)
Inductive all (X : Type) (P : X -> Prop) : list X -> Prop :=

(* Assignment06_05.v *)
Inductive all {X : Type} (P : X -> Prop) : list X -> Prop :=

When you use {X:Type}, you should hide your type X, so all X P l is not permitted and Coq can inference the type from just all P l, but if you really want to indicate the type explicitly, you have to use @all X P l instead.

[alkaza]

If all X P l is not permitted, then what do you do?

On Tue, Apr 21, 2015 at 8:13 PM, jaewooklee93 notifications@github.com wrote:

I guess their difference is {X:Type} and (X:Type).

(* MoreLogic.v *)Inductive all (X : Type) (P : X -> Prop) : list X -> Prop :=

(* Assignment06_05.v *)Inductive all {X : Type} (P : X -> Prop) : list X -> Prop :=

When you use {X:Type}, you should hide your type, so all X P l is not permitted, but if you really want to indicate the type, you have to type @all X P l instead.

— Reply to this email directly or view it on GitHub https://github.com/snu-sf/pl2015/issues/75#issuecomment-94748226.

[alkaza]

Ah, nevermind, got it. Thank you very much!

On Tue, Apr 21, 2015 at 8:33 PM, Alena Kazakova alenadanse@gmail.com wrote:

If all X P l is not permitted, then what do you do?

On Tue, Apr 21, 2015 at 8:13 PM, jaewooklee93 notifications@github.com wrote:

I guess their difference is {X:Type} and (X:Type).

(* MoreLogic.v *)Inductive all (X : Type) (P : X -> Prop) : list X -> Prop :=

(* Assignment06_05.v *)Inductive all {X : Type} (P : X -> Prop) : list X -> Prop :=

When you use {X:Type}, you should hide your type, so all X P l is not permitted, but if you really want to indicate the type, you have to type @all X P l instead.

— Reply to this email directly or view it on GitHub https://github.com/snu-sf/pl2015/issues/75#issuecomment-94748226.