def ssnd

bend-collections-laws-math@1.0.0.0 · proofs/lib/logic.bend:117

import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as Logic
import Base

117def ssnd(-A: Type, -B: @-x: A -> Type, p: Sigma<&1, &1, A, B>) -> B(sfst(A, B, p)):
118  match p:
119    case Tuple{a, b}:
120      b

Uses (2)

Used by (0)

No other definition uses this definition.