RuleFile.AaFp.bit: def of bend-osdev-apparmor@0.1.0.0
Import: import bend-osdev-apparmor@0.1.0.0/rule_file.bend as RuleFile
Lines 157-185 of bend-osdev-apparmor@0.1.0.0/rule_file.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-apparmor@0.1.0.0/rule_file.bend&start_line=157&end_line=185

import Base

# one of the access letters r w a l k m (n: its bit), or a bare x (n = 6)
def AaFp.bit(f: AaFp, n: Nat) -> AaFp:
  match f:
    case AaFp{st, r, w, a, l, k, m, e, b, ok}:
      match n:
        case 0n:
          AaFp{AaFpBase{}, True{}, w, a, l, k, m, e, b, ok}
        case 1n+n1:
          match n1:
            case 0n:
              AaFp{AaFpBase{}, r, True{}, a, l, k, m, e, b, ok}
            case 1n+n2:
              match n2:
                case 0n:
                  AaFp{AaFpBase{}, r, w, True{}, l, k, m, e, b, ok}
                case 1n+n3:
                  match n3:
                    case 0n:
                      AaFp{AaFpBase{}, r, w, a, True{}, k, m, e, b, ok}
                    case 1n+n4:
                      match n4:
                        case 0n:
                          AaFp{AaFpBase{}, r, w, a, l, True{}, m, e, b, ok}
                        case 1n+n5:
                          match n5:
                            case 0n:
                              AaFp{AaFpBase{}, r, w, a, l, k, True{}, e, b, ok}
                            case 1n+n6:
                              AaFp{AaFpBase{}, r, w, a, l, k, m, e, True{}, ok}

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/rule_file.bend&name=AaFp
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/rule_file.bend&name=AaFpSt