~/jendhub

def equal_reflexive

stelliferous@0.0.2.0 · proofs/nat_order.bend:114

import stelliferous@0.0.2.0/proofs/nat_order.bend as NatOrder
import Base

114def equal_reflexive(+value: Nat) -> {Nat.is_eq(value,value) == True{} : Bool}:
115  match value:
116    case 0n: {==}
117    case 1n+rest: equal_reflexive(rest)

Uses (3)

Used by (1)