Michael Soegtrop (Mar 04 2024 at 11:02): Michael Soegtrop (Mar 04 2024 at 11:02):Related to the above question, I tried:
pred type-is-prop i:term.
type-is-prop TERM :- coq.typecheck TERM (sort prop) _ .
Which does not work - it also succeeds on set and type. I guess this is so because the second argument of coq.typecheck is mode o, but I thought o is the general case and i restricts to matches with the head of the rule (rather than unification). So I don't quite understand, what is going on here. I also tried o for the mode of the argument of type-is-prop (since the argument in the only rule head is a variable, so one must unify), but this also didn't work
This does work:
pred type-is-prop i:term.
type-is-prop TERM :- coq.typecheck TERM TYPE _, TYPE = sort prop .
don't you need to say ok? otherwise it can produce coq.typecheck Set Prop (Error "cannot unify Type1 and Prop")
Michael Soegtrop (Mar 04 2024 at 11:17):@Gaëtan Gilbert : thanks! Always the right answer :-)
I can confirm that this does work:
pred type-is-prop o:term.
type-is-prop TERM :- coq.typecheck TERM (sort prop) ok.
Michael Soegtrop has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC