Agda equivalent of `destruct <term> eqn:<identifier>`

Question

I understand that Agda does case analysis using with-clauses, which is similar Coq's destruct tactic. The destruct tactic has a variant of the form destruct <term> eqn:<identifier>, which additionally adds to the context an equation between <term> and the value that <term> takes in each case. Is there an analogous way to add this equation to context in Agda?

Answer 1

You need to use the inspect idiom which will do exactly what you require.

I have described thoroughly how to use it in the following answer:

`with f x` matches `false`, but cannot construct `f x == false`