Commit f870cdaf by Ralf Jung

### actually create the ndisj HintDb. this makes it unfold constants so that we can use 'Hint Resolve'.

parent 21fbbdde
Pipeline #3993 passed with stage
in 3 minutes and 27 seconds
 ... @@ -87,13 +87,12 @@ of the forms: ... @@ -87,13 +87,12 @@ of the forms: - [N1 ⊥ N2] - [N1 ⊥ N2] - [↑N1 ⊆ E ∖ ↑N2 ∖ .. ∖ ↑Nn] - [↑N1 ⊆ E ∖ ↑N2 ∖ .. ∖ ↑Nn] - [E1 ∖ ↑N1 ⊆ E2 ∖ ↑N2 ∖ .. ∖ ↑Nn] *) - [E1 ∖ ↑N1 ⊆ E2 ∖ ↑N2 ∖ .. ∖ ↑Nn] *) Create HintDb ndisj. Hint Resolve ndisj_subseteq_difference : ndisj. Hint Resolve ndisj_subseteq_difference : ndisj. Hint Extern 0 (_ ⊥ _) => apply ndot_ne_disjoint; congruence : ndisj. Hint Extern 0 (_ ⊥ _) => apply ndot_ne_disjoint; congruence : ndisj. Hint Extern 1 (_ ⊥ _) => apply ndot_preserve_disjoint_l : ndisj. Hint Resolve ndot_preserve_disjoint_l ndot_preserve_disjoint_r Hint Extern 1 (_ ⊥ _) => apply ndot_preserve_disjoint_r : ndisj. nclose_subseteq' ndisj_difference_l : ndisj. Hint Extern 1 (_ ⊆ _) => apply nclose_subseteq' : ndisj. Hint Resolve namespace_subseteq_difference_l | 100 : ndisj. Hint Resolve namespace_subseteq_difference_l | 100 : ndisj. Hint Resolve ndisj_difference_l : ndisj. Ltac solve_ndisj := Ltac solve_ndisj := repeat match goal with repeat match goal with ... ...
• Maintainer

Nice catch. Any idea why this is so? Is this documented behavior? If not, it looks inconsistent, so we should create a bug report.

• Maintainer
• Maintainer

Excellent!

Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!