undocumented idris2 features

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