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

Documentation

data FreeVars Source

Constructors

FV
Fields 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