Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.Abstract.UsedNames

Synopsis

- allUsedNames :: Expr -> Set Name

# Documentation

allUsedNames :: Expr -> Set Name Source #

All names used in an abstract expression. This is used when rendering clauses to figure out which (implicit) pattern variables must be preserved. For example, the for `f : Nat → Nat`, the clause `f {n} = 0` can be printed as `f = 0` (dropping the `n`), but `f {n} = n` must preserve the `n`.