| Agda-2.2.6: 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
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.
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

Produced by Haddock version 2.4.2