AlphaGitHub
Source/Packages

Std.Numeric.Profile

packages/foundation/standard/src/Std/Numeric/Profile.alpha

736 lines139 declarations26.5 KiBSHA-256 2450517e3794
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 379–388

stdProfilesBothExact

Full file
the common subset of two profiles (PRD 19: the cross-target gate of System A): an operation both realize exactly
379def stdProfilesBothExact =
380  (lambda unrestricted a : (family StdNumericProfile) .
381    (lambda unrestricted b : (family StdNumericProfile) .
382      (lambda unrestricted operation : (family StdNumericOperation) .
383        (nat-eliminate
384          (lambda unrestricted current : Nat . Nat)
385          zero
386          (lambda unrestricted predecessor : Nat .
387            (lambda unrestricted induction : Nat . (stdProfileExact b operation)))
388          (stdProfileExact a operation)))))

The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.