Agda-2.2.10: 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 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