Zulip Chat Archive

Stream: new members

Topic: tactic.cases_core


Kenny Lau (Nov 24 2018 at 09:56):

What is the output of tactic.cases_core?

Mario Carneiro (Nov 24 2018 at 10:04):

/-- Apply `cases_on` recursor, names for the new hypotheses are retrieved from `ns`.
   `h` must be a local constant. It returns for each new goal the name of the constructor, a list of new hypotheses, and a list of
   substitutions for hypotheses depending on `h`. The number of new goals may be smaller than the
   number of constructors. Some goals may be discarded when the indices to not match.
   See `induction` for information on the list of substitutions.

   The `cases` tactic is implemented using this one, and it relaxes the restriction of `h`. -/

Kenny Lau (Nov 24 2018 at 18:36):

I don't really understand a list of substitutions for hypotheses and the fact that sometimes I get duplicates in that particular list


Last updated: Dec 20 2023 at 11:08 UTC