# Zulip Chat Archive

## Stream: new members

### Topic: cases alternative

#### Sarah Mameche (Dec 18 2018 at 21:32):

Hi, using `cases`

on an hypothesis sometimes gives me really huge terms in the resulting hypotheses. It's happened if the hypothesis contains recursive definitions, and I fixed it in one case by marking the definition as `irreducible`

.

However, now I get the same problem for the definition

def Fin : nat → Type | 0 := empty | (n+1) := option (Fin n)

as soon as I call cases on something like `x: Fin (n+1)`

. In Coq, this goes through, so I guess it has something to do with definitions being compiled to recursors? Is there another way to use cases without unfolding the definition/getting this huge expression? (Marking Fin as irreducible didn't work because I want to match on it in other proofs)

#### Kevin Buzzard (Dec 18 2018 at 22:25):

Definitions made with the equation compiler in Lean can sometimes come out quite unwieldy. Does it make any difference if you just apply the recursor directly?

#### Kevin Buzzard (Dec 18 2018 at 22:26):

def Fin' : nat → Type := λ n, nat.rec_on n (empty) (λ n Fn, option Fn)

#### Chris Hughes (Dec 18 2018 at 22:30):

A definition like this one in `number_theory/dioph`

is probably easier to use, and gives a similar induction principle

inductive fin2 : ℕ → Type | fz {n} : fin2 (succ n) | fs {n} : fin2 n → fin2 (succ n)

#### Sarah Mameche (Dec 18 2018 at 23:05):

That helped, thanks!

Last updated: May 15 2021 at 23:13 UTC