~/jendhub

def bool_decode_encode

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

import qasim-bend-kit@0.1.0.2/proof/AES_CertificateProof.bend as AESCertificateProof
import Base

33def bool_decode_encode(+a: Bool, +b: Bool, +proof: {a == b : Bool}) ->
34    {bool_decode(a, b, bool_encode(a, b, proof)) == proof : {a == b : Bool}}:
35    %path@proof : {bool_decode(a, _, bool_encode(a, _, path)) == path :
36        {a == _ : Bool}}
37    bool_decode_refl(a)

Uses (4)

Used by (1)