Agda-2.2.10: A dependently typed functional programming language and proof assistant
Source code
Contents
Index
Agda.TypeChecking.MetaVars.Occurs
Synopsis
data
OccursCtx
=
Flex
|
Rigid
abort
::
OccursCtx
->
TypeError
->
TCM
()
class
Occurs
t
where
occurs
::
OccursCtx
->
MetaId
-> [
Nat
] -> t ->
TCM
t
occursCheck
::
MonadTCM
tcm =>
MetaId
-> [
Nat
] ->
Term
-> tcm
Term
hasBadRigid
:: [
Nat
] ->
Term
->
Bool
killArgs
:: [
Bool
] ->
MetaId
->
TCM
Bool
killedType
:: [(
Arg
(
String
,
Type
),
Bool
)] ->
Type
-> ([
Arg
Bool
],
Type
)
performKill
:: [
Arg
Bool
] ->
MetaId
->
Type
->
TCM
()
Documentation
data
OccursCtx
Source
Constructors
Flex
Rigid
abort
::
OccursCtx
->
TypeError
->
TCM
()
Source
class
Occurs
t
where
Source
Extended occurs check.
Methods
occurs
::
OccursCtx
->
MetaId
-> [
Nat
] -> t ->
TCM
t
Source
occursCheck
::
MonadTCM
tcm =>
MetaId
-> [
Nat
] ->
Term
-> tcm
Term
Source
When assigning
m xs := v
, check that
m
does not occur in
v
and that the free variables of
v
are contained in
xs
.
hasBadRigid
:: [
Nat
] ->
Term
->
Bool
Source
killArgs
:: [
Bool
] ->
MetaId
->
TCM
Bool
Source
killedType
:: [(
Arg
(
String
,
Type
),
Bool
)] ->
Type
-> ([
Arg
Bool
],
Type
)
Source
performKill
:: [
Arg
Bool
] ->
MetaId
->
Type
->
TCM
()
Source
Produced by
Haddock
version 2.6.1