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
viewLsb' (modNatNZ n 2 nz) (divNatNZ n 2 nz) (boundModNatNZ n 2 nz)
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)
blah n with (2 * n)
blah n | w = ?blah_rhs
w : Nat
n : Nat
------------------------------
blah_rhs : w = w
blah2 : (n : Nat) -> 2 * n = n + (n + 0)
blah2 n with %syntactic (2 * n)
blah2 n | w = ?blah2_rhs
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)
blah n with (2 * n) proof eq
blah n | w = ?blah_rhs
w : Nat
n : Nat
eq : plus n (plus n 0) = w
------------------------------
blah_rhs : w = w