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).
3 questions
7
votes
2
answers
175
views
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 ...
- 355
2
votes
1
answer
222
views
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 ...
- 73
1
vote
1
answer
62
views
In LEAN4 prover, what's the problem of generalising a type from String to a free type?
I'd like to convert the following code in Coq to Lean 4:
(this is the beginning of the soundness proof of type system F-)
...
- 131