Agda-2.2.6: A dependently typed functional programming language and proof assistant
Source code
Contents
Index
Agda.TypeChecking.MetaVars.Occurs
Synopsis
class
Occurs
t
where
occurs
:: (
TypeError
->
TCM
()
) ->
MetaId
-> [
Nat
] -> t ->
TCM
t
occursCheck
::
MonadTCM
tcm =>
MetaId
-> [
Nat
] ->
Term
-> tcm
Term
Documentation
class
Occurs
t
where
Source
Extended occurs check.
Methods
occurs
:: (
TypeError
->
TCM
()
) ->
MetaId
-> [
Nat
] -> t ->
TCM
t
Source
Instances
Occurs
Sort
Occurs
Type
Occurs
Term
Occurs
a =>
Occurs
([] a)
Occurs
a =>
Occurs
(
Arg
a)
Occurs
a =>
Occurs
(
Abs
a)
(
Occurs
a,
Occurs
b) =>
Occurs
(
(,)
a b)
occursCheck
::
MonadTCM
tcm =>
MetaId
-> [
Nat
] ->
Term
-> tcm
Term
Source
Produced by
Haddock
version 2.4.2