Agda.Interaction.MakeCase
- findClause :: MetaId -> TCM (QName, Clause)
- makeCase :: InteractionId -> Range -> String -> TCM [Clause]
- prettySplitError :: SplitError -> TCM Doc
- makeAbsurdClause :: QName -> SplitClause -> TCM Clause
- makeAbstractClause :: QName -> SplitClause -> TCM Clause
- deBruijnIndex :: Expr -> TCM Nat
Documentation
findClause :: MetaId -> TCM (QName, Clause)Source
Find the clause whose right hand side is the given meta. Raises an error if there is no such clause.
makeAbsurdClause :: QName -> SplitClause -> TCM ClauseSource
makeAbstractClause :: QName -> SplitClause -> TCM ClauseSource
deBruijnIndex :: Expr -> TCM NatSource