blog/posts/idris2-features.md

103 lines
2.4 KiB
Markdown
Raw Normal View History

2023-05-03 16:00:19 -04:00
---
title: undocumented idris2 features
date: 2022-11-12
tags: [computer, idris]
header-includes: |
<style>
.sidebyside {
display: grid;
grid-template-columns: 1fr 1fr;
}
.sidebyside :is(.input, .goal) {
box-sizing: border-box;
width: 95%;
height: 95%;
}
.sidebyside .input { grid-area: 0 / 1; }
.sidebyside .goal { grid-area: 1 / 2; }
</style>
...
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][viewLsb]:
```idris
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
viewLsb' (modNatNZ n 2 nz) (divNatNZ n 2 nz) (boundModNatNZ n 2 nz)
```
[viewLsb]: https://git.rhiannon.website/rhi/quox/src/branch/ope/lib/Quox/NatExtra.idr#L110-L116
## 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)`:
:::sidebyside
``` {.idris .input}
blah : (n : Nat) -> 2 * n = n + (n + 0)
blah n with (2 * n)
blah n | w = ?blah_rhs
```
``` {.idris .goal}
w : Nat
n : Nat
------------------------------
blah_rhs : w = w
```
``` {.idris .input}
blah2 : (n : Nat) -> 2 * n = n + (n + 0)
blah2 n with %syntactic (2 * n)
blah2 n | w = ?blah2_rhs
```
``` {.idris .goal}
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.
:::sidebyside
``` {.idris .input}
blah : (n : Nat) -> 2 * n = n + (n + 0)
blah n with (2 * n) proof eq
blah n | w = ?blah_rhs
```
``` {.idris .goal}
w : Nat
n : Nat
eq : plus n (plus n 0) = w
------------------------------
blah_rhs : w = w
```
:::