def Digits

bend-trace-context@0.2.0.0 · src/digits.bend:26

import bend-trace-context@0.2.0.0/src/digits.bend as Digits

import Base

26# The type of sequences of exactly n digits, computed from n: Digits(0n) is
27# Digits.Nil and Digits(1n+p) is Digits.Con<p>.
28def Digits(n: Nat) -> Data:
29  match n:
30    case 0n:
31      Digits.Nil
32    case 1n+p:
33      Digits.Con<p>

Uses (3)

Used by (23)