I have inductively defined Foo (m: nat) f
defined alike
Inductive Foo (m: nat) f :=
| Foo0 : Bar f -> Foo 0 f
| FooS : forall (m: nat), Baz (Foo m) f -> Foo m.+1 f
Then, I destructured it as follows.
(* I had a hypothesis (Hm: Foo m.+1 f) here *)
case Eq: m'.+1 f / Hm=> //.
Now I got bunch of variables like _m_
, _f_
introduced.
I heard this method of inversion gives me more control, so I did not expect this.
Why is this happening? Is there a way to assign names that I want?
I also cannot use these hypothesis, it says "identifier is reserved".
IIRC you can introduce them (and give names) after the =>. Usually ssreflect would let you leave them in the goal, but that'd be ill-typed here, since you're introducing Eq.
Thank you! I was confused because it gave a branch, so I needed to introduce variables for each branch.
abab9579 has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC