Merge pull request #135 from mattheww/2023-09_rulenames

nikomatsakis · web-flow · commit f9a50cbccde8 · 2023-09-18T10:23:24.000-04:00
Rename some rules
diff --git a/crates/formality-prove/src/prove/prove_eq.rs b/crates/formality-prove/src/prove/prove_eq.rs
@@ -63,7 +63,7 @@ judgment_fn! {
 
         (
             (prove_existential_var_eq(decls, env, assumptions, v, r) => c)
-            ----------------------------- ("existential-nonvar")
+            ----------------------------- ("existential")
             (prove_eq(decls, env, assumptions, Variable::ExistentialVar(v), r) => c)
         )
 
@@ -102,7 +102,7 @@ judgment_fn! {
 
         (
             (if env.universe(p) < env.universe(v))
-            ----------------------------- ("existential-placeholder")
+            ----------------------------- ("existential-universal")
             (prove_existential_var_eq(_decls, env, _assumptions, v, Variable::UniversalVar(p)) => (env, (v, p)))
         )
     }
diff --git a/crates/formality-prove/src/prove/prove_wc.rs b/crates/formality-prove/src/prove/prove_wc.rs
@@ -111,7 +111,7 @@ judgment_fn! {
 
         (
             (prove_wf(decls, env, assumptions, p) => c)
-            ----------------------------- ("trait ref is local")
+            ----------------------------- ("parameter well formed")
             (prove_wc(decls, env, assumptions, Relation::WellFormed(p)) => c)
         )
 

Original file line number	Diff line number	Diff line change
`@@ -63,7 +63,7 @@ judgment_fn! {`
`63`	`63`
`64`	`64`	`(`
`65`	`65`	`(prove_existential_var_eq(decls, env, assumptions, v, r) => c)`
`66`		`- ----------------------------- ("existential-nonvar")`
	`66`	`+ ----------------------------- ("existential")`
`67`	`67`	`(prove_eq(decls, env, assumptions, Variable::ExistentialVar(v), r) => c)`
`68`	`68`	`)`
`69`	`69`
`@@ -102,7 +102,7 @@ judgment_fn! {`
`102`	`102`
`103`	`103`	`(`
`104`	`104`	`(if env.universe(p) < env.universe(v))`
`105`		`- ----------------------------- ("existential-placeholder")`
	`105`	`+ ----------------------------- ("existential-universal")`
`106`	`106`	`(prove_existential_var_eq(_decls, env, _assumptions, v, Variable::UniversalVar(p)) => (env, (v, p)))`
`107`	`107`	`)`
`108`	`108`	`}`
Original file line number	Diff line number	Diff line change
`@@ -111,7 +111,7 @@ judgment_fn! {`
`111`	`111`
`112`	`112`	`(`
`113`	`113`	`(prove_wf(decls, env, assumptions, p) => c)`
`114`		`- ----------------------------- ("trait ref is local")`
	`114`	`+ ----------------------------- ("parameter well formed")`
`115`	`115`	`(prove_wc(decls, env, assumptions, Relation::WellFormed(p)) => c)`
`116`	`116`	`)`
`117`	`117`