def power

stelliferous@0.0.2.0 · proofs/word_power_of_two.bend:6

import Base

6def power(+width: Nat,depth: Nat) -> Word(width):
7  match width:
8    case 0n:
9      WNil{}
10    case 1n+rest:
11      match depth:
12        case 0n:
13          WCon{True{},Word.zero(rest)}
14        case 1n+previous:
15          WCon{False{},power(rest,previous)}