~/jendhub

def word.eq_tail

bend-osdev-algo@0.1.0.0 · PROOF.bend:1014

import bend-osdev-algo@0.1.0.0/PROOF.bend as PROOF
import Base

1014def word.eq_tail(c: Cmp, x: Bool, y: Bool, e: {Cmp.is_eq(Word.cmp.fin(x, y, c)) == True{} : Bool}) -> {Cmp.is_eq(c) == True{} : Bool}:
1015  match c:
1016    case LT{}:
1017      Empty.absurd({False{} == True{} : Bool}, absurd.ft(e))
1018    case EQ{}:
1019      {==}
1020    case GT{}:
1021      Empty.absurd({False{} == True{} : Bool}, absurd.ft(e))

Uses (6)

Used by (1)