| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Agda.TypeChecking.Injectivity
- headSymbol :: Term -> TCM (Maybe TermHead)
- checkInjectivity :: QName -> [Clause] -> TCM FunctionInverse
- functionInverse :: Term -> TCM InvView
- data InvView
- data MaybeAbort
- useInjectivity :: Comparison -> Type -> Term -> Term -> TCM ()
Documentation
checkInjectivity :: QName -> [Clause] -> TCM FunctionInverse Source
functionInverse :: Term -> TCM InvView Source
Argument should be in weak head normal form.
data MaybeAbort Source
useInjectivity :: Comparison -> Type -> Term -> Term -> TCM () Source