zohaze (Oct 26 2021 at 00:11): zohaze (Oct 26 2021 at 00:11):I have natural number n as input argument in a function. Have pattern matching on it , It may be 0 or S n'. When I perform induction I get 0 & S n. S n is some greater number of n. But it should be S n'( any number not necessary greater).Why this happen?
Paolo Giarrusso (Oct 26 2021 at 00:56):S n is not a bigger number than the original n, because it uses an unrelated n.
Paolo Giarrusso (Oct 26 2021 at 00:59):the tactic "induction n" removes the original n from the context, and introduces an unrelated n.
Last updated: Sep 23 2023 at 07:01 UTC