def wbit

lawful-words@0.1.0.0 · proof_word.bend:777

import Base

777# Bit k of a word (False from n up).
778def wbit(n: Nat, w: Word(n), k: Nat) -> Bool:
779  match n:
780    case 0n:
781      False{}
782    case 1n+p:
783      match w:
784        case WCon{b, t}:
785          match k:
786            case 0n:
787              b
788            case 1n+j:
789              wbit(p, t, j)