def last

bend-collections-laws-math@1.0.0.0 · proofs/lib/lemmas/src/wide.bend:17

import Base

17def last(n: Nat, w: Word(n)) -> Bool:
18  match n:
19    case 0n:
20      False{}
21    case 1n+0n:
22      match w:
23        case WCon{b, tail}:
24          b
25    case 1n+1n+p:
26      match w:
27        case WCon{b, tail}:
28          last(1n+p, tail)