if these are already in the documentation somewhere, i didn’t find it.

## quantities on case, let, with

occasionally, idris can’t infer that these expressions should be non-ω. usually when there are still holes in the definition, it seems. so you can specify the quantity you want directly after the keyword, for example:

```
export
viewLsb : (n : Nat) -> ViewLsb n
=
viewLsb n -- ↓ here
let 0 nz : NonZero 2 = %search in
rewrite DivisionTheorem n 2 nz nz in
rewrite multCommutative (divNatNZ n 2 nz) 2 in
2 nz) (divNatNZ n 2 nz) (boundModNatNZ n 2 nz) viewLsb' (modNatNZ n
```

## syntactic with-abstraction

using `with`

can be costly, since it has to evaluate the expression being abstracted, as well as the types of the goal and bound variables, to find occurrences of it. maybe you know they are all already syntactically equal. in that case, you can say `… with %syntactic (expr)`

:

```
blah : (n : Nat) -> 2 * n = n + (n + 0)
with (2 * n)
blah n | w = ?blah_rhs blah n
```

```
w : Nat
n : Nat
------------------------------
blah_rhs : w = w
```

```
blah2 : (n : Nat) -> 2 * n = n + (n + 0)
with %syntactic (2 * n)
blah2 n | w = ?blah2_rhs blah2 n
```

```
w : Nat
n : Nat
------------------------------
blah2_rhs : w = plus n (plus n 0)
```

in `blah2`

, only the exact syntactic occurrence of `2 * n`

is replaced, and the `n + (n + 0)`

is left alone.

## equality proof in with

a `with`

-abstraction can *also* have a proof of equality between the pattern and the original expression, like the old inspect pattern.

```
blah : (n : Nat) -> 2 * n = n + (n + 0)
with (2 * n) proof eq
blah n | w = ?blah_rhs blah n
```

```
w : Nat
n : Nat
eq : plus n (plus n 0) = w
------------------------------
blah_rhs : w = w
```