def word_same_refl

bendtorch-core@0.1.0.0 · src/tensor/permutation_mapping.bend:545

import bendtorch-core@0.1.0.0/src/tensor/permutation_mapping.bend as PermutationMapping
import Base
import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout

545def word_same_refl(+width: Nat, +word: Word(width)) -> {Layout.word_same(width, word, word) == True{} : Bool}:
546  match width:
547    case 0n:
548      {==}
549    case 1n+p:
550      match word:
551        case WCon{False{}, +tail}:
552          word_same_refl(p, tail)
553        case WCon{True{}, +tail}:
554          word_same_refl(p, tail)

Uses (5)

Used by (1)