~/jendhub

def word_fin_b

lawful-words@0.1.0.0 · proof_word.bend:273

import lawful-words@0.1.0.0/proof_word.bend as ProofWord
import Base

273def word_fin_b(+ab: Bool, +bb: Bool, +t: Cmp, e: {Word.cmp.fin(ab, bb, t) == EQ{} : Cmp}) -> {Bool.cmp(ab, bb) == EQ{} : Cmp}:
274  match t:
275    case LT{}:
276      Empty.absurd({Bool.cmp(ab, bb) == EQ{} : Cmp}, lt_ne_eq(e))
277    case EQ{}:
278      e
279    case GT{}:
280      Empty.absurd({Bool.cmp(ab, bb) == EQ{} : Cmp}, gt_ne_eq(e))

Uses (7)

Used by (1)