Stream: Coq users

Topic: show type of expression under context

view this post on Zulip yiyuan-cao (Jun 28 2023 at 06:11):

Is it possible to show the type of a subexpression in Coq? Or to print the local typing context at a particular "program hole" (Like Agda) ? It would be really useful for debugging ill-typed dependent pattern matching.

view this post on Zulip Paolo Giarrusso (Jun 28 2023 at 12:02):

In proof mode, you can provide a partial expression with the refine tactic, using underscores for holes.

Last updated: Oct 13 2024 at 01:02 UTC