~/jendhub

def cmp_eq_of_true

qasim-bend-kit@0.1.0.2 · proof/AES_StringEqProof.bend:13

import qasim-bend-kit@0.1.0.2/proof/AES_StringEqProof.bend as AESStringEqProof
import Base

13def cmp_eq_of_true(c: Cmp,
14    accepted: {Cmp.is_eq(c) == True{} : Bool}) -> {c == EQ{} : Cmp}:
15    match c:
16        case EQ{}: {==}
17        case LT{}: Empty.absurd({LT{} == EQ{} : Cmp}, false_true(accepted))
18        case GT{}: Empty.absurd({GT{} == EQ{} : Cmp}, false_true(accepted))

Uses (5)

Used by (1)