4f8db64e23
fix(simplifier): missing simp rule in prop simplifier fix(library/unfold_macros): do not look for untrusted macros when using sufficient trust level
31 lines
1.2 KiB
Text
31 lines
1.2 KiB
Text
open tactic
|
|
|
|
universe variable l
|
|
constants (ss₁ : Type.{l} → Type.{l})
|
|
(ss₂ : Π {A : Type.{l}}, A → Type.{l})
|
|
[sss₁ : ∀ T, subsingleton (ss₁ T)]
|
|
[sss₂ : ∀ T (t : T), subsingleton (ss₂ t)]
|
|
(A B : Type.{l}) (HAB : A = B)
|
|
(ss_A : ss₁ A) (ss_B : ss₁ B)
|
|
(a₁ a₁' a₂ a₂' : A)
|
|
(H₁ : a₁ = a₁') (H₂ : a₂ = a₂')
|
|
(ss_a₁ : ss₂ a₁)
|
|
(ss_a₁' : ss₂ a₁')
|
|
(ss_a₂ : ss₂ a₂)
|
|
(ss_a₂' : ss₂ a₂')
|
|
(f : Π (X : Type.{l}) (ss_X : ss₁ X) (x₁ x₂ : X) (ss_x₁ : ss₂ x₁) (ss_x₂ : ss₂ x₂), Type.{l})
|
|
|
|
attribute sss₁ [instance]
|
|
attribute sss₂ [instance]
|
|
|
|
attribute HAB [simp]
|
|
attribute H₁ [simp]
|
|
attribute H₂ [simp]
|
|
|
|
example : f A ss_A a₁ a₂ ss_a₁ ss_a₂ = f A ss_A a₁' a₂' ss_a₁' ss_a₂' := by simp
|
|
|
|
attribute [reducible] definition c₁' := a₁'
|
|
attribute [reducible] definition c₂' := a₂'
|
|
|
|
example : f A ss_A a₁' a₂' ss_a₁' ss_a₂' = f A ss_A c₁' c₂' ss_a₁' ss_a₂' := by simp
|
|
example : f A ss_A a₁ a₂ ss_a₁ ss_a₂ = f A ss_A c₁' c₂' ss_a₁' ss_a₂' := by simp
|