Agda-2.2.10: 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 solved metas, but collects the variables from a metavariable application
X ts
as
flexibleVars
.
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.6.1