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

- 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

Constructors

FV |

Fields

rigidVars :: Set Nat
flexibleVars :: Set Nat

class Free a

Doesn't go inside solved metas, but collects the variables from a metavariable application `X ts` as `flexibleVars`.

Instances

Free ClauseBody |
Free Sort |
Free Type |
Free Term |
Free a => Free [a] |
Free a => Free (Arg a) |
Free a => Free (Abs a) |
Free a => Free (Tele a) |
(Free a, Free b) => Free (a, b) |

freeVars :: Free a => a -> FreeVars

allVars :: FreeVars -> Set Nat

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

freeInIgnoringSorts :: Free a => Nat -> a -> Bool