Agda-2.2.6: A dependently typed functional programming language and proof assistant
Agda.TypeChecking.Free
Description
Computing the free variables of a term.
Synopsis
data FreeVars Source
Constructors
Fields
class Free a Source
Doesn't go inside metas.
Instances
freeVars :: Free a => a -> FreeVarsSource
allVars :: FreeVars -> Set NatSource
freeIn :: Free a => Nat -> a -> BoolSource
freeInIgnoringSorts :: Free a => Nat -> a -> BoolSource