CODEWITHSUNDEEP
coq
Audition
Audition

Reputation: 13

Coq Error: Illegal application (Non-functional construction)

New to coq, I'm trying to make a notation for Less than or equal to, for my arithmetic expressions syntax. EDIT: I added my data type for expressions.

My expressions data type:

Inductive Exp :=
| num : nat -> Exp
| var : string -> Exp
| add : Exp -> Exp -> Exp
| sub : Exp -> Exp -> Exp
| div : Exp-> Exp -> Exp.

My condition data type:

Inductive Cond :=
| base : bool -> Cond
| bnot : Cond -> Cond
| beq  : Exp -> Exp -> Cond 
| less : Exp -> Exp -> Cond
| band : Cond -> Cond -> Cond.

As you can see, I don't have a constructor for Less than or equal to, that's just the way our teacher intended for the exercise to be. So I have to make use of the other constructors when making my notation for Less than or equal to. This is what I have:

Notation "A <=' B" := (bnot (band (bnot (beq A B) bnot(less A B)))) (at level 10).

Now when I try to check the type of this following expression:

Check "x" <=' "y".

I get the following error:

Illegal application (Non-functional construction): 
The expression "! "x" =' "y"" of type 
"Cond"
cannot be applied to the term
 "bnot" : "Cond -> Cond"

Any help is appreciated, thank you.

Upvotes: 1

Views: 146

Answers (1)

Li-yao Xia
Li-yao Xia

Reputation: 33399

There are missing parentheses in your notation.

(* no  *) Notation "A <=' B" := (bnot (band (bnot (beq A B) bnot(less A B)))) (at level 10).

(* yes *) Notation "A <=' B" := (bnot (band (bnot (beq A B)) (bnot(less A B)))) (at level 10).

Upvotes: 1

Related Questions