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
occursCheck
::
MonadTCM
tcm =>
MetaId
-> [
Nat
] ->
Term
-> tcm
Term
Source
Produced by
Haddock
version 2.6.0