The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

On May 7, 2015, at 18:17 , Vadim Zaliva <vzaliva AT cmu.edu> wrote:

Error: Illegal application (Non-functional construction): 

The _expression_ "Vcons A a" of type "vector Type (S ?n)"

cannot be applied to the term

 "n" : "nat"

I am using latest build from v8.5 branch.

Sorry, wrote too fast. Replacing VCons in your definition with Vector.cons worked. I was using previous

example which has this notation defined:

Notation Vcons n t := (@Vector.cons _ n _ t).

Sincerely,
Vadim Zaliva

--

CMU ECE PhD candidate

Mobile: +1(510)220-1060

Skype: vzaliva