Agda.Syntax.Abstract.UsedNames

Documentation

allUsedNames :: Expr -> Set Name

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.