def h.at1

bend-kit-collections@0.1.4.1 · PROOF.bend:1830

import Base

1830def h.at1(n: Nat, w: Word(n)) -> Bool:
1831  match n:
1832    case 0n:
1833      True{}
1834    case 1n+p:
1835      match w:
1836        case WCon{b, t}:
1837          match b:
1838            case True{}:
1839              h.isz(p, t)
1840            case False{}:
1841              h.at1(p, t)