coq-serapi icon indicating copy to clipboard operation
coq-serapi copied to clipboard

TypeOf only gives the type of identifiers, not of expressions.

Open darbyhaller opened this issue 6 years ago • 2 comments
trafficstars

For example, (Query (TypeOf "S")) returns the correct result, however (Query (TypeOf "S O")) results in the error (CErrors.UserError ("" "Invalid character ' ' in identifier \"S O\".")))

darbyhaller avatar Sep 19 '19 19:09 darbyhaller

Indeed TypeOf only admits identifiers at the moment; hopefully will take care of that in the new query language.

ejgallego avatar Sep 19 '19 20:09 ejgallego

You could give it a go, however there is the issue of choice of input representation that we still didn't handle at all.

ejgallego avatar Sep 19 '19 20:09 ejgallego