chore(tests/lean/run): adjust tests
This commit is contained in:
parent
9a4a12899a
commit
b6bac2e542
2 changed files with 3 additions and 3 deletions
|
@ -10,7 +10,7 @@ begin
|
||||||
exact finset.card fxs
|
exact finset.card fxs
|
||||||
end
|
end
|
||||||
|
|
||||||
example {T : Type} (xs : set T) [fn₁ fn₂ : finite_set xs] : @card T xs fn₁ = @card T xs fn₂ :=
|
example {T : Type} (xs : set T) [fn₁ : finite_set xs] [fn₂ : finite_set xs] : @card T xs fn₁ = @card T xs fn₂ :=
|
||||||
begin
|
begin
|
||||||
induction fn₁ with fxs₁ h₁,
|
induction fn₁ with fxs₁ h₁,
|
||||||
induction fn₂ with fxs₂ h₂,
|
induction fn₂ with fxs₂ h₂,
|
||||||
|
@ -18,7 +18,7 @@ begin
|
||||||
apply sorry
|
apply sorry
|
||||||
end
|
end
|
||||||
|
|
||||||
example {T : Type} (xs : set T) [fn₁ fn₂ : finite_set xs] : @card T xs fn₁ = @card T xs fn₂ :=
|
example {T : Type} (xs : set T) [fn₁ : finite_set xs] [fn₂ : finite_set xs] : @card T xs fn₁ = @card T xs fn₂ :=
|
||||||
begin
|
begin
|
||||||
induction fn₁ with fxs₁ h₁,
|
induction fn₁ with fxs₁ h₁,
|
||||||
induction fn₂ with fxs₂ h₂,
|
induction fn₂ with fxs₂ h₂,
|
||||||
|
|
|
@ -4,7 +4,7 @@ print raw ((Prop))
|
||||||
print raw Prop
|
print raw Prop
|
||||||
print raw fun (x y : Prop), x x
|
print raw fun (x y : Prop), x x
|
||||||
print raw fun (x y : Prop) {z : Prop}, x y
|
print raw fun (x y : Prop) {z : Prop}, x y
|
||||||
print raw λ [x y : Prop] {z : Prop}, x z
|
print raw λ [x : Prop] [y : Prop] {z : Prop}, x z
|
||||||
print raw Pi (x y : Prop) {z : Prop}, x
|
print raw Pi (x y : Prop) {z : Prop}, x
|
||||||
print raw ∀ (x y : Prop) {z : Prop}, x
|
print raw ∀ (x y : Prop) {z : Prop}, x
|
||||||
print raw forall {x y : Prop} w {z : Prop}, x
|
print raw forall {x y : Prop} w {z : Prop}, x
|
||||||
|
|
Loading…
Add table
Reference in a new issue