Computing the free variables of a term.
Documentation
Doesn't go inside solved metas, but collects the variables from a
metavariable application X ts
as flexibleVars
.
freeInIgnoringSorts :: Free a => Nat -> a -> BoolSource
Computing the free variables of a term.
Doesn't go inside solved metas, but collects the variables from a
metavariable application X ts
as flexibleVars
.
freeInIgnoringSorts :: Free a => Nat -> a -> BoolSource