Fields

• locationFilePath :: Maybe FilePath
   
• locationLine :: Maybe Int
   
• locationColumn :: Maybe Int
   

Fields

• varType :: TermT n
   
• varValue :: Maybe (TermT n)
   
• varModality :: TModality
   
• varModAccum :: TModality
   
• varOrig :: Binder

  the names the binder introduced, for display only

• varIsAssumption :: Bool
   
• varIsTopLevel :: Bool
   
• varDeclaredAssumptions :: [Name n]
   
• varLocation :: Maybe LocationInfo
   
• varDataRole :: Maybe (DataRole n)

  the role the entry plays for a #data declaration, if any

• varMetaPrefix :: Int

  the length of the entry's meta-parameter prefix (0 for locals and for declarations with no meta parameters); see Rzk.TypeCheck.MetaPrefix. Recomputed when a section close rewrites the entry's type.

Fields

• dataRoleDataType :: Name n

  the type former this entry belongs to

• dataRoleNumParams :: Int

  the datatype parameters the entry takes before anything else

• dataRoleKind :: DataRoleKind
   

Fields

• tModAccum :: TModality
   
• tModVar :: TModality
   
• tTope :: TermT n
   

Fields

• ctxScope :: Scope n

  Every name in scope: the top-level entries, the section assumptions and the binders entered on the way here. Substitution and freshness need it.

• ctxVars :: NameMap n (VarInfo n)

  What each name in scope stands for. Total on ctxScope, which is what lookupName assumes.

• ctxNamed :: Map VarIdent (Name n)

  The surface name of each top-level entry (and of each named binder), for resolving an identifier the parser produced.

• ctxBound :: [Name n]

  Every name in scope, most recently bound first.

  The order has to be recorded, not recovered: free-foil refreshes a binder only when its name clashes, so after a substitution an inner binder may well carry a smaller id than an outer one (\ x2 -> \ x1 -> …), and the ascending order of ctxVars is not the order things were bound in. Display depends on this: names claim their display name oldest-first, so that an inner binder is the one refreshed away from an outer name, and not the other way round.

• ctxSections :: [SectionInfo n]

  The open sections, innermost first. Each records the entries declared in it, so closing it can turn them into declarations.

• ctxDiscreteTopes :: [ModalTope n]

  Discreteness axioms for the flat cube variables in scope (a flat point of 2 or I is an endpoint). Maintained at binder entry, so entailment does not rescan the context on every query.

• ctxTopes :: [ModalTope n]
   
• ctxTopesNF :: [ModalTope n]
   
• ctxTopesNFUnion :: [[ModalTope n]]
   
• ctxTopesEntailBottom :: Maybe Bool
   
• ctxTopesSaturated :: CachedSaturation n

  The saturated alternatives for this tope context, cached at the points where the tope context changes.

• ctxShadow :: Map VarIdent [VarIdent]

  The identifiers in scope, keyed by their spelling (a VarIdent compares by spelling and carries the position of its defining occurrence, so the values are what a shadowing report names).

  The check runs at every binder entry, and scanning every name in scope each time was O(context) per binder — with every top-level definition of a project in scope, that is most of them.

• ctxActionStack :: [Action n]
   
• ctxActionStackDepth :: Int

  The length of ctxActionStack, maintained alongside it: measuring the list on every judgement made each action cost O(depth), and each path O(depth²).

• ctxCurrentCommand :: Maybe Command
   
• ctxLocation :: Maybe LocationInfo
   
• ctxVerbosity :: Verbosity
   
• ctxCovariance :: Covariance
   
• ctxRenderBackend :: Maybe RenderBackend
   
• ctxRenderHideTerm :: Bool

  When rendering a diagram, hide the proof term: drop the <title> (which carries the full term) from every cell and blank the visible label of proof-coloured (interior) cells, keeping the given boundary labels.

• ctxHolesAreErrors :: Bool

  When True (the default), an unfilled hole is reported as a TypeErrorUnsolvedHole; finished work (and CI) must have no holes. The lenient mode (allowHoles) instead records each hole's goal and context.

• ctxDeferHoleMismatches :: Bool

  How holes behave during unification, giving three modes overall. With ctxHolesAreErrors a hole is rejected outright (strict). Otherwise a hole always unifies as a leaf; this flag then chooses what happens when the surrounding structure disagrees: True (the default) defers — any term containing a hole is accepted, for an in-progress sketch — while False keeps such a mismatch an error (structuralHoleUnify).

• ctxHintLemmas :: [VarIdent]

  Named top-level definitions a hole's candidate list may draw on, beyond the local hypotheses (see withHintLemmas).

• ctxWarnOverhang :: Bool

  When True, a restriction face or recOR guard that overhangs the local tope context (is not entailed by it, while still overlapping it) is reported with a non-fatal hint. Off by default: deciding the overhang costs a solver entailment per face and guard, and the overhang is legitimate (see happy-restrict-face-not-contained). Enabled with #set-option "warn-overhang" "yes". The disjointness error next to it is unaffected: a vacuous face is always rejected.

• ctxMetaPrefixSensitivity :: MetaPrefixSensitivity

  How sensitively the meta-parameter layer check classifies use positions (see Rzk.TypeCheck.MetaPrefix). Strict by default; set with #set-option "warn-meta-prefix" = "off" | "structural" | "strict".

Fields

• sectionName :: Maybe SectionName
   
• sectionEntries :: [Name n]