The Coq mailing list

[""Savi Maharaj"" <savi AT cs.stir.ac.uk>]

Hello,

I am playing around with the "Correctness" tactic and would like some
more information about the types that I am allowed to use in annotated
programs. My impression is that, according to the manual (Section
16.2.2) any cic_term may be used as a type. However, the syntax of
expressions (Fig 16.1) is much more limited. So, for example, I can
introduce a variable l of type "list nat", but I cannot then write
expressions such as "head l", so what I can actually do with l is
very limited.

Am I right about this? Is there any workaround that would allow me to
write simple programs over (non-polymorphic) lists? I have been trying
to code up simple examples such as "length", "append" etc.

Savi Maharaj