Agda equivalent of `destruct eqn:`

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 eqn:, which additionally adds to the context an equation between and the value that takes in each case. Is there an analogous way to add this equation to context in Agda?

user_8988486 · Answer

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`

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

1 Answers