Judgment `prove_existential_var_eq`

judgment_fn! {
    pub fn prove_existential_var_eq(
        _decls: Program,
        env: Env,
        assumptions: Predicates,
        v: ExistentialVar,
        b: Parameter,
    ) => Constraints {
        /* rules omitted */
    }
}

Source: crates/formality-rust/src/prove/prove_eq.rs:76

The 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
94	2	(if let None = t.downcast::<Variable>())
95	3	(equate_variable(decls, env, assumptions, v, t) => c)
		──────── ("existential-nonvar")
97	56	(prove_existential_var_eq(decls, env, assumptions, v, t) => c)

existential-existential

Line	Coverage	Source
120	N/A	(let (a, b) = env.order_by_universe(l, r))
		──────── ("existential-existential")
122	21	(prove_existential_var_eq(_decls, env, _assumptions, l, Variable::ExistentialVar(r)) => (env, (b, a)))

existential-universal

Line	Coverage	Source
140	2	(if env.universe(p) < env.universe(v))
		──────── ("existential-universal")
142	214	(prove_existential_var_eq(_decls, env, _assumptions, v, Variable::UniversalVar(p)) => (env, (v, p)))

How to read this page

Keyboard shortcuts

A MIR Formality

Judgment prove_existential_var_eq

Judgment `prove_existential_var_eq`