Commit ea51b43b authored by Ralf Jung's avatar Ralf Jung
Browse files

perf experiment: dont make frame_fractional an instance

parent f85824ee
......@@ -194,7 +194,8 @@ Section fractional.
Global Existing Instances frame_fractional_hyps_l frame_fractional_hyps_r
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
FrameFractionalHyps p R Φ RES r q
Frame p R P RES. (* No explicit priority, as default prio > [frame_here]'s 1. *)
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment