def bool_code

qasim-bend-kit@0.1.0.2 · proof/AES_CertificateProof.bend:3

import Base

3# Decidable equality makes certificates for Bool and Nat unique. These lemmas
4# compare proofs without evaluating the computation that produced each proof.
5def bool_code(a: Bool, b: Bool) -> Data:
6    match a b:
7        case False{} False{}: Unit
8        case True{} True{}: Unit
9        case _ _: Empty