| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

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 Doc | Source

makeAbsurdClause :: QName -> SplitClause -> TCM Clause | Source

makeAbstractClause :: QName -> SplitClause -> TCM Clause | Source

deBruijnIndex :: Expr -> TCM Nat | Source

Produced by Haddock version 2.4.2