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
ApplicationsCategory TheoryExpression InterpreterBuild Simulator
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

Generic

Reflection over levitated descriptions and datatype macro outputs. Datatype consumers should use this layer instead of raw _dtypeMeta. Generic algebraic ornament helpers check algebra descriptors against generic.desc.shape; the supported fragment is ret/arg/rec/plus. Ornament validation exposes total structured diagnostics for expected surface errors; semantic ornament maps remain pure over validated inputs. Functional ornaments expose manual sections for canonical base-to-ornamented construction; synthesis is layered on later. The first synthesis layer accepts { base; spec; synth; }, reuses the ordinary ornament spec, and requires explicit builders for inserted fields. Proof-marked inserted fields use prove or synth.constructors.<name>.proofs and report unresolved proof obligations as structured diagnostics. Declared measures feed algebraic/measure-derived inserted fields through the synthesis builder context and produce missing-measure obligations. Function transport lifts base producers and transforms through canonical functional output sections while existing pullback remains forget-then-run.

path

path: list-level operations on a [Position] descent chain — empty, extend, render, renderAll. Position segments themselves are constructed via fx.diag.positions (P.Field name, P.Elem i, etc.); this module only handles the list assembly and pretty-rendering.

path : { empty, extend, render, renderAll }

Operations on a path (a list of Position segments naming a structural descent from a validation root to a failure site):

  • empty = [] is the root path.
  • extend : Path -> Position -> Path appends a segment.
  • render : Position -> String pretty-renders one segment.
  • renderAll : Path -> String concatenates rendered segments.

Position segments are produced by fx.diag.positions (the canonical curried constructors Field, Elem, Tag, Tuple, plus the ~30 nullary description/MLTT positions). Handlers consume the same Position records regardless of whether they come from kernel descent or value-side verify= walks.

Sub-namespaces

Source

prevRegistryDescnext