coq-serapi
coq-serapi copied to clipboard
TypeOf only gives the type of identifiers, not of expressions.
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\".")))
Indeed TypeOf only admits identifiers at the moment; hopefully will take care of that in the new query language.
You could give it a go, however there is the issue of choice of input representation that we still didn't handle at all.