Skip to content
Snippets Groups Projects
Commit 5bae01cc authored by Ralf Jung's avatar Ralf Jung
Browse files

perf experiment: dont make frame_fractional an instance

parent 255341dd
No related branches found
No related tags found
No related merge requests found
...@@ -194,7 +194,8 @@ Section fractional. ...@@ -194,7 +194,8 @@ Section fractional.
Global Existing Instances frame_fractional_hyps_l frame_fractional_hyps_r Global Existing Instances frame_fractional_hyps_l frame_fractional_hyps_r
frame_fractional_hyps_half. frame_fractional_hyps_half.
Global Instance frame_fractional p R r Φ P q RES: (* Not an instance because of performance; you can locally add it if you are willing to pay the cost. *)
Lemma frame_fractional p R r Φ P q RES:
AsFractional R Φ r AsFractional P Φ q AsFractional R Φ r AsFractional P Φ q
FrameFractionalHyps p R Φ RES r q FrameFractionalHyps p R Φ RES r q
Frame p R P RES. (* No explicit priority, as default prio > [frame_here]'s 1. *) Frame p R P RES. (* No explicit priority, as default prio > [frame_here]'s 1. *)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment