Skip to content
This repository has been archived by the owner on Apr 25, 2020. It is now read-only.

Commit

Permalink
move type class short circuits out of section
Browse files Browse the repository at this point in the history
this takes 35% off the compile time of the file
  • Loading branch information
robertylewis committed Aug 22, 2019
1 parent 63ebf91 commit 658b120
Showing 1 changed file with 2 additions and 1 deletion.
3 changes: 2 additions & 1 deletion src/sensitivity.lean
Original file line number Diff line number Diff line change
Expand Up @@ -172,9 +172,10 @@ def add_comm_monoid : add_comm_monoid (V n) := by apply_instance
def has_scalar : has_scalar ℝ (V n) := by apply_instance
def has_add : has_add (V n) := by apply_instance

end V

local attribute [instance, priority 100000]
V.module V.add_comm_semigroup V.add_comm_monoid V.has_scalar V.has_add
end V

/-- The basis of V indexed by the hypercube, defined inductively. -/
noncomputable def e : Π {n}, Q n → V n
Expand Down

0 comments on commit 658b120

Please sign in to comment.