Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

Agda.TypeChecking.Injectivity

Synopsis

- reduceHead :: Term -> TCM (Blocked Term)
- headSymbol :: Term -> TCM (Maybe TermHead)
- checkInjectivity :: QName -> [Clause] -> TCM FunctionInverse
- functionInverse :: Term -> TCM InvView
- data InvView
  - = Inv QName Args (Map TermHead Clause)
  - | NoInv
- useInjectivity :: Comparison -> Type -> Term -> Term -> TCM ()

# Documentation

reduceHead :: Term -> TCM (Blocked Term)

Reduce simple (single clause) definitions.

headSymbol :: Term -> TCM (Maybe TermHead)

checkInjectivity :: QName -> [Clause] -> TCM FunctionInverse

functionInverse :: Term -> TCM InvView

Argument should be on weak head normal form.

data InvView

Constructors

Inv QName Args (Map TermHead Clause) |
NoInv |

useInjectivity :: Comparison -> Type -> Term -> Term -> TCM ()