Agda-2.2.4: 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 where freeVars :: a -> FreeVars allVars :: FreeVars -> Set Nat freeIn :: Free a => Nat -> a -> Bool

Documentation

data FreeVars Source

Constructors FV rigidVars :: Set Nat flexibleVars :: Set Nat

class Free a where Source

Doesn't go inside metas. Methods freeVars :: a -> FreeVars Source Instances Free ClauseBody Free Telescope 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)

allVars :: FreeVars -> Set Nat Source

freeIn :: Free a => Nat -> a -> Bool Source

Produced by Haddock version 2.4.2