Navigation
Manual
GuideIntroductionGetting StartedEffects and HandlersTyped ValidationGenerated DatatypesGeneric ProgrammingOrnaments and Description-Backed DataProof GuideSugar
ConceptsTheory
InternalsTrampolineSystems ArchitectureKernel ArchitectureKernel Formal Specification
Examples
Overview
ProofsProof BasicsEquality ProofsVerified Functions
Effects and ValidationHandler-Swap Validation
Surface LanguagesSurface STLCSTLC Core SurfaceSTLC Sums and ProductsSTLC Recursive ListsSTLC Refinements and Diagnostics
API Reference
Core APIKernelCompBindsTrampolineQueueAdaptPipelineStateThunkSugarBuildTypesExperimentalDesc-interpComposeCompose-lawsComposed-shortcutComposed-shortcut-lawsDescDescind-lawsEffectsErrorError-shortcut-lawsError-uniform-shortcut-lawsStateState-shortcut-lawsExtractKernelTrampoline
DiagnosticsPositionsErrorHintsPretty
EffectsStateReaderWriterAccErrorConditionsChoiceScopeLinearTypecheckHasHandler
TypesFoundationPrimitivesConstructorsRefinementDependentLinearUniverse
StreamsCoreTransformLimitCombineReduce
Type CheckerTermValueQuoteConvEval_internalDispatchCheckDiag_internalElaborateMeta_internalHoas_internal_encoders_forced_indexedSurfaceRegistryGenericDescDatatypeValueDeriveCheckCheckDOrnamentsVerified
Diagnostic HintsDArgSort::universe-mismatchDPiSort::universe-mismatchLevelMaxLhs::type-mismatchLevelMaxRhs::type-mismatchLevelSucPred::type-mismatchULevel::type-mismatchAnnType::not-a-typeJType::not-a-typeMotive.PiDom::not-a-typeMotive::not-a-typePiCod::not-a-typePiDom::not-a-typeDArgBody::not-a-descDPiBody::not-a-descDPlusL::not-a-descDPlusR::not-a-descDRecTail::not-a-descMuDesc::not-a-descAppHead::not-a-functionDPiFn::not-a-functionMotive::not-a-functionOpaqueType::not-a-functionDPiFn::type-mismatchDRecIndex::type-mismatchDRetIndex::type-mismatchMuIndex::type-mismatchMuPayload::type-mismatchElem::inhabitation-failedField::inhabitation-failedSigmaFst::inhabitation-failedSigmaSnd::inhabitation-failedTag::inhabitation-failedElem::refinement-failedField::refinement-failedSigmaFst::refinement-failedSigmaSnd::refinement-failedTag::refinement-failedCase::type-mismatchScrut::type-mismatchAnnTerm::type-mismatchAppArg::type-mismatchJType::type-mismatchOpaqueType::type-mismatch::unhandled-boot-inl::unhandled-boot-inr::unhandled-boot-refl::unhandled-lam::unhandled-other::unhandled-pair::unhandled-tt

Compose-laws

fx.experimental.desc-interp.compose-laws: kernel-checked one-shot meta-theorem for composeHandlers. Two clauses (inl/inr); both discharge by H.refl.

composeHandlersInlLemma

Inl clause proof: 12 lams + H.refl. checkHoas succeeds because kernel conv decides composeHandlers' iota universally.

composeHandlersInlLemmaTy

Inl clause Π-type: composeHandlers on (inl op_A, pair s_A s_B) ≡ sumElim … (H_A op_A s_A) (mkResume_composed …) (mkAbort_composed …) with s_B threaded.

composeHandlersInrLemma

Inr clause proof: 12 lams + H.refl.

composeHandlersInrLemmaTy

Inr clause Π-type: mirror of the inl clause with the state-slot roles swapped.

prevComposeComposed-shortcutnext