Skip to main content

Questions tagged [free-variables]

An occurrence of a variable in a logic formula which is not inside the scope of a quantifier. (from Wolfram MathWorld).

Filter by
Sorted by
Tagged with
2 votes
1 answer

Higher Observational Type Theory: variables becoming free in reduction rules

This question is based on the talks given by Mike Shulman on higher observational type theory (part 1, part 2, part 3). In trying to understand the reduction rules of the calculus, I tried to work ...
6 votes
2 answers

Policies on introducing free variables when rewriting?

When using a fact like x = y <=> x + z = y + z as a rewrite rule, it can be desirable to introduce an unused free variable into the result of the rewrite ...