Agda-2.2.6: A dependently typed functional programming language and proof assistant
Source code
Contents
Index
Agda.TypeChecking.Free
Description
Computing the free variables of a term.
Synopsis
data
FreeVars
=
FV
{
rigidVars
::
Set
Nat
flexibleVars
::
Set
Nat
}
class
Free
a
freeVars
::
Free
a => a ->
FreeVars
allVars
::
FreeVars
->
Set
Nat
freeIn
::
Free
a =>
Nat
-> a ->
Bool
freeInIgnoringSorts
::
Free
a =>
Nat
-> a ->
Bool
Documentation
data
FreeVars
Source
Constructors
FV
rigidVars
::
Set
Nat
flexibleVars
::
Set
Nat
class
Free
a
Source
Doesn't go inside metas.
Instances
Free
ClauseBody
Free
Telescope
Free
Sort
Free
Type
Free
Term
Free
a =>
Free
([] a)
Free
a =>
Free
(
Arg
a)
Free
a =>
Free
(
Abs
a)
(
Free
a,
Free
b) =>
Free
(
(,)
a b)
freeVars
::
Free
a => a ->
FreeVars
Source
allVars
::
FreeVars
->
Set
Nat
Source
freeIn
::
Free
a =>
Nat
-> a ->
Bool
Source
freeInIgnoringSorts
::
Free
a =>
Nat
-> a ->
Bool
Source
Produced by
Haddock
version 2.4.2