def aes_nat_eq_proof

qasim-bend-kit@0.1.0.2 · libs/AES256GCM.bend:318

import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES256GCM

import Base

318def aes_nat_eq_proof(+a: Nat, +b: Nat) -> Maybe<&0, {a == b : Nat}>:
319    match a b:
320        case 0n 0n: Some{{==}}
321        case 0n 1n+p: None{}
322        case 1n+p 0n: None{}
323        case 1n+pa 1n+pb: aes_nat_eq_step(pa, pb, aes_nat_eq_proof(pa, pb))

Uses (3)

Used by (16)