~/jendhub

def sfst

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

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

111# Dependent pair projections (call results cannot be destructured directly).
112def sfst(-A: Type, -B: @-x: A -> Type, p: Sigma<&1, &1, A, B>) -> A:
113  match p:
114    case Tuple{a, b}:
115      a

Uses (1)

Used by (1)