Stream: Elpi users & devs

Topic: How to get the type of a term

view this post on Zulip Michael Soegtrop (Mar 04 2024 at 09:36):

I couldn't find a primitive which for a given Coq term returns the type of this term as a Coq term. Specifically I want to check if the type of the type of a binder is Prop or something else.

view this post on Zulip Pierre Roux (Mar 04 2024 at 09:46):

What about coq.typecheck ?

Last updated: Oct 13 2024 at 01:02 UTC