Gabriel Ebner
Gabriel Ebner
1. Call `:LeanTermGoal` twice, this opens a floating window and moves the cursor into it. 2. Open a nested popup and move the cursor into the nested popup. (requires Lean...
The important ones are `# headlines`, `*emphasis*`, and `` `inline code` ``.
Didn't manage to add this in #138: > What's missing is the "show tooltip when moving the cursor over a term" feature (right now you still need to click). From...
```scala val Some(ugly) = Escargot.getExpansionProof(hof"∃x ∃y (p(x) → p(y))") // :- ∃x ∃y (p(x) → p(y)) // +^{x, y} (wk-{p(x)} → p(y)+) // +^{y, y} (p(y)- → wk+{p(y)}) ``` :disappointed:...
The principle of function extensionality states that pointwise equal functions are equal, that is, they can be used interchangeably. This can simplify proofs considerably since we do not need to...
Apparently the change from `Process.!` to `runProcess` caused dozens of java processes to run at the same time. Could this issue also appear with the external prover interfaces?
## Example 1. Clearly the following formula is valid: `P(x) -> ∀x P(x)` 2. After substitution it is no longer valid: `P(x) -> ∀x P(x)` What is happening here? As...
Example: ``` scala val x = FOLVar("x") val y = FOLVar("y") All(x, y===y).replace(LambdaPosition(2,1,2), x) ``` returns `∀x.y=x`, but should probably return `∀x0.y=x` (i.e. rename the bound variable). This probably has...
~1 page, induction-to-schema conversion, struct, characteristic formula, whatever works nicely
Right before gaptic section. * Polymorphic lambda calculus * Recursive definitions