Skip to content

Instantly share code, notes, and snippets.

@kbuzzard

kbuzzard/pattern.lean

Created August 8, 2018 12:40
Show Gist options
  • Save kbuzzard/8b4048c89309808fe829c5e59caaa503 to your computer and use it in GitHub Desktop.
Save kbuzzard/8b4048c89309808fe829c5e59caaa503 to your computer and use it in GitHub Desktop.
Download ZIP
pattern we're trying to rewrite
Raw
pattern.lean
Pattern we're trying to rewrite:
@finset.sum.{0 0} nat
(@mv_polynomial.{0 0} nat rat
(@comm_ring.to_comm_semiring.{0} rat
(@nonzero_comm_ring.to_comm_ring.{0} rat
(@integral_domain.to_nonzero_comm_ring.{0} rat
(@field.to_integral_domain.{0} rat
(@linear_ordered_field.to_field.{0} rat
(@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat
rat.discrete_linear_ordered_field)))))))
(@add_comm_group.to_add_comm_monoid.{0}
(@mv_polynomial.{0 0} nat rat
(@comm_ring.to_comm_semiring.{0} rat
(@nonzero_comm_ring.to_comm_ring.{0} rat
(@integral_domain.to_nonzero_comm_ring.{0} rat
(@field.to_integral_domain.{0} rat
(@linear_ordered_field.to_field.{0} rat
(@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat
rat.discrete_linear_ordered_field)))))))
(@module.to_add_comm_group.{0 0} rat
(@mv_polynomial.{0 0} nat rat
(@comm_ring.to_comm_semiring.{0} rat
(@nonzero_comm_ring.to_comm_ring.{0} rat
(@integral_domain.to_nonzero_comm_ring.{0} rat
(@field.to_integral_domain.{0} rat
(@linear_ordered_field.to_field.{0} rat
(@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat
rat.discrete_linear_ordered_field)))))))
(@comm_ring.to_ring.{0} rat
(@nonzero_comm_ring.to_comm_ring.{0} rat
(@integral_domain.to_nonzero_comm_ring.{0} rat
(@field.to_integral_domain.{0} rat
(@linear_ordered_field.to_field.{0} rat
(@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat
rat.discrete_linear_ordered_field))))))
(@mv_polynomial.module.{0 0} rat nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : rat), rat.decidable_eq a b)
(@nonzero_comm_ring.to_comm_ring.{0} rat
(@integral_domain.to_nonzero_comm_ring.{0} rat
(@field.to_integral_domain.{0} rat
(@linear_ordered_field.to_field.{0} rat
(@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat
rat.discrete_linear_ordered_field))))))))
(finset.range (@has_add.add.{0} nat nat.has_add k (@has_one.one.{0} nat nat.has_one)))
(λ (i : nat),
@has_mul.mul.{0}
(@mv_polynomial.{0 0} nat rat
(@comm_ring.to_comm_semiring.{0} rat
(@nonzero_comm_ring.to_comm_ring.{0} rat
(@integral_domain.to_nonzero_comm_ring.{0} rat
(@field.to_integral_domain.{0} rat
(@linear_ordered_field.to_field.{0} rat
(@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat
rat.discrete_linear_ordered_field)))))))
(@mv_polynomial.has_mul.{0 0} rat nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : rat), rat.decidable_eq a b)
(@comm_ring.to_comm_semiring.{0} rat
(@nonzero_comm_ring.to_comm_ring.{0} rat
(@integral_domain.to_nonzero_comm_ring.{0} rat
(@field.to_integral_domain.{0} rat
(@linear_ordered_field.to_field.{0} rat
(@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat
rat.discrete_linear_ordered_field)))))))
(@has_pow.pow.{0 0}
(@mv_polynomial.{0 0} nat rat
(@comm_ring.to_comm_semiring.{0} rat
(@nonzero_comm_ring.to_comm_ring.{0} rat
(@integral_domain.to_nonzero_comm_ring.{0} rat
(@field.to_integral_domain.{0} rat
(@linear_ordered_field.to_field.{0} rat
(@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat
rat.discrete_linear_ordered_field)))))))
nat
(@monoid.has_pow.{0}
(@mv_polynomial.{0 0} nat rat
(@comm_ring.to_comm_semiring.{0} rat
(@nonzero_comm_ring.to_comm_ring.{0} rat
(@integral_domain.to_nonzero_comm_ring.{0} rat
(@field.to_integral_domain.{0} rat
(@linear_ordered_field.to_field.{0} rat
(@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat
rat.discrete_linear_ordered_field)))))))
(@ring.to_monoid.{0}
(@mv_polynomial.{0 0} nat rat
(@comm_ring.to_comm_semiring.{0} rat
(@nonzero_comm_ring.to_comm_ring.{0} rat
(@integral_domain.to_nonzero_comm_ring.{0} rat
(@field.to_integral_domain.{0} rat
(@linear_ordered_field.to_field.{0} rat
(@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat
rat.discrete_linear_ordered_field)))))))
(@mv_polynomial.ring.{0 0} rat nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : rat), rat.decidable_eq a b)
(@nonzero_comm_ring.to_comm_ring.{0} rat
(@integral_domain.to_nonzero_comm_ring.{0} rat
(@field.to_integral_domain.{0} rat
(@linear_ordered_field.to_field.{0} rat
(@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat
rat.discrete_linear_ordered_field))))))))
(@mv_polynomial.C.{0 0} rat nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : rat), rat.decidable_eq a b)
(@comm_ring.to_comm_semiring.{0} rat
(@nonzero_comm_ring.to_comm_ring.{0} rat
(@integral_domain.to_nonzero_comm_ring.{0} rat
(@field.to_integral_domain.{0} rat
(@linear_ordered_field.to_field.{0} rat
(@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat
rat.discrete_linear_ordered_field))))))
(@coe.{1 1} nat rat
(@coe_to_lift.{1 1} nat rat
(@coe_base.{1 1} nat rat (@nat.cast_coe.{0} rat rat.has_zero rat.has_one rat.has_add)))
(@nat.Prime.p _inst_1)))
i)
(@has_pow.pow.{0 0}
(@mv_polynomial.{0 0} nat rat
(@comm_ring.to_comm_semiring.{0} rat
(@nonzero_comm_ring.to_comm_ring.{0} rat
(@integral_domain.to_nonzero_comm_ring.{0} rat
(@field.to_integral_domain.{0} rat
(@linear_ordered_field.to_field.{0} rat
(@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat
rat.discrete_linear_ordered_field)))))))
nat
(@monoid.has_pow.{0}
(@mv_polynomial.{0 0} nat rat
(@comm_ring.to_comm_semiring.{0} rat
(@nonzero_comm_ring.to_comm_ring.{0} rat
(@integral_domain.to_nonzero_comm_ring.{0} rat
(@field.to_integral_domain.{0} rat
(@linear_ordered_field.to_field.{0} rat
(@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat
rat.discrete_linear_ordered_field)))))))
(@ring.to_monoid.{0}
(@mv_polynomial.{0 0} nat rat
(@comm_ring.to_comm_semiring.{0} rat
(@nonzero_comm_ring.to_comm_ring.{0} rat
(@integral_domain.to_nonzero_comm_ring.{0} rat
(@field.to_integral_domain.{0} rat
(@linear_ordered_field.to_field.{0} rat
(@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat
rat.discrete_linear_ordered_field)))))))
(@mv_polynomial.ring.{0 0} rat nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : rat), rat.decidable_eq a b)
(@nonzero_comm_ring.to_comm_ring.{0} rat
(@integral_domain.to_nonzero_comm_ring.{0} rat
(@field.to_integral_domain.{0} rat
(@linear_ordered_field.to_field.{0} rat
(@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat
rat.discrete_linear_ordered_field))))))))
(@mv_polynomial.X.{0 0} rat nat (λ (a b : nat), nat.decidable_eq a b)
(λ (a b : rat), rat.decidable_eq a b)
(@comm_ring.to_comm_semiring.{0} rat
(@nonzero_comm_ring.to_comm_ring.{0} rat
(@integral_domain.to_nonzero_comm_ring.{0} rat
(@field.to_integral_domain.{0} rat
(@linear_ordered_field.to_field.{0} rat
(@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat
rat.discrete_linear_ordered_field))))))
i)
(@has_pow.pow.{0 0} nat nat nat.has_pow (@nat.Prime.p _inst_1) (@has_sub.sub.{0} nat nat.has_sub k i))))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment