def internal_word_cmp_refl

bend-mathlib@0.8.1.0 · string.bend:128

import Base
import bend-mathlib@0.8.1.0/bool.bend as MBool

128def internal_word_cmp_refl(n: Nat, w: Word(n)) -> {EQ{} == Word.cmp(n, w, w) : Cmp}:
129  match n:
130    case 0n:
131      {==}
132    case 1n+p:
133      match w:
134        case WCon{ab, at}:
135          %internal_word_cmp_refl(p, at) : {EQ{} == Word.cmp.fin(ab, ab, _) : Cmp}
136          %Equal.sym(Cmp, Bool.cmp(ab, ab), EQ{}, MBool.cmp_refl(ab)) : {EQ{} == _ : Cmp}
137          {==}