# Zulip Chat Archive

## Stream: general

### Topic: int.sizeof

#### Enrico Borba (Jan 16 2020 at 06:05):

I'm trying to define `fib`

over the naturals, but I can't seem to make the equation compiler happy. I tried writing

def fib : ℤ → ℤ | (int.of_nat 0) := 0 | (int.of_nat 1) := 1 | (int.of_nat (n + 2)) := fib (n + 1) + fib n | -[1+ n] := fib (-(1 + n) + 1) - fib (-(1 + n) + 2)

I need to prove a few things to have well founded recursion, one of them is `int.sizeof ↑n < n + 3`

. Using `#print`

I can see the definition of `int.sizeof`

and see that the statement I need to show is true. I couldn't find any docs on `int.sizeof`

though, and I also don't see it in `int.basic`

, what is it and why is it showing up here?

#### Mario Carneiro (Jan 16 2020 at 07:04):

I recommend breaking this into two definitions

#### Mario Carneiro (Jan 16 2020 at 07:05):

The equation compiler will accept the definition over `nat`

, and the definition over `int`

can refer to it in each branch

#### Mario Carneiro (Jan 16 2020 at 07:07):

If you see the equation compiler giving you subgoals about `X.sizeof`

, that just means it failed to prove it automatically and you need to supply your own well founded measure. `X.sizeof`

is almost never the measure you want to use

#### Enrico Borba (Jan 16 2020 at 18:42):

Splitting them up worked. Thank you for that suggestion.

Last updated: May 11 2021 at 21:10 UTC