Curated kernel terms for production/reference differential checks.
Summary
Functions
Returns reference-kernel checking cases.
Returns rejected checking cases for production/reference comparison.
Returns defeq cases for production/reference comparison.
Returns reference-kernel inference cases.
Returns rejected inference cases for production/reference comparison.
Returns normalization cases for production/reference comparison.
Types
@type check_case() :: {atom(), Theoria.Term.t(), Theoria.Term.t()}
@type check_rejection_case() :: {atom(), Theoria.Term.t(), Theoria.Term.t()}
@type defeq_case() :: {atom(), Theoria.Term.t(), Theoria.Term.t()}
@type infer_case() :: {atom(), Theoria.Term.t()}
@type infer_rejection_case() :: {atom(), Theoria.Term.t()}
@type normalize_case() :: {atom(), Theoria.Term.t()}
Functions
@spec check_cases() :: [check_case()]
Returns reference-kernel checking cases.
@spec check_rejection_cases() :: [check_rejection_case()]
Returns rejected checking cases for production/reference comparison.
@spec defeq_cases() :: [defeq_case()]
Returns defeq cases for production/reference comparison.
@spec infer_cases() :: [infer_case()]
Returns reference-kernel inference cases.
@spec infer_rejection_cases() :: [infer_rejection_case()]
Returns rejected inference cases for production/reference comparison.
@spec normalize_cases() :: [normalize_case()]
Returns normalization cases for production/reference comparison.