Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Interaction.MakeCase
Synopsis
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.
makeCase :: InteractionId -> Range -> String -> TCM [Clause]Source
prettySplitError :: SplitError -> TCM DocSource
makeAbsurdClause :: QName -> SplitClause -> TCM ClauseSource
makeAbstractClause :: QName -> SplitClause -> TCM ClauseSource
deBruijnIndex :: Expr -> TCM NatSource
Produced by Haddock version 2.6.0