Safe Haskell	None
Language	Haskell2010

Mikan.TypeChecking.Rules.Cubical

Description

This module implements the rules for type-checking the side conditions imposed on the "constrained" cubical primitives (Kan operations, constructors for glue/hcomp{U}, Partial disjunction).

Synopsis

cubicalPrimChecks :: Map PrimitiveId (QName -> ArgsCheck)
isConstrainedPrimitive :: QName -> TCM (Maybe ArgsCheck)

Documentation

cubicalPrimChecks :: Map PrimitiveId (QName -> ArgsCheck) Source #

Map associating the identifier of a cubical primitive to a function which checks its argument spine.

The continuation receives the QName through which the primitive function was applied to generate proper error messages in case of e.g. renaming.

isConstrainedPrimitive :: QName -> TCM (Maybe ArgsCheck) Source #

Check whether the given name (which must be defined) corresponds to a cubical primitive with constraints on its argument spine and, if so, return the function to check them.