Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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.
show/hide Instances
freeVars :: Free a => a -> FreeVarsSource
allVars :: FreeVars -> Set NatSource
freeIn :: Free a => Nat -> a -> BoolSource
freeInIgnoringSorts :: Free a => Nat -> a -> BoolSource
Produced by Haddock version 2.4.2