Judgment prove_existential_var_eq at crates/formality-rust/src/prove/prove/prove/prove_eq.rs:78
Signature:
prove_existential_var_eq(_decls: Program, env: Env, assumptions: Wcs, v: ExistentialVar, b: Parameter,) => ConstraintsThe number on each rule’s conclusion is positive coverage; the number on each premise is negative coverage. Click a number to browse the tests.
existential-nonvar| Line | Coverage | Source |
|---|---|---|
| 96 | 2 | (if let None = t.downcast::<Variable>()) |
| 97 | 3 | (equate_variable(decls, env, assumptions, v, t) => c) |
| ──────── ("existential-nonvar") | ||
| 99 | 31 | (prove_existential_var_eq(decls, env, assumptions, v, t) => c) |
existential-existential| Line | Coverage | Source |
|---|---|---|
| 122 | N/A | (let (a, b) = env.order_by_universe(l, r)) |
| ──────── ("existential-existential") | ||
| 124 | 7 | (prove_existential_var_eq(_decls, env, _assumptions, l, Variable::ExistentialVar(r)) => (env, (b, a))) |