Agda-2.6.4: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Syntax.Abstract.UsedNames

Synopsis

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.