From b6bac2e5422ac6f2387a061f73e556ccc9692515 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 13 Dec 2015 12:23:44 -0800 Subject: [PATCH] chore(tests/lean/run): adjust tests --- tests/lean/run/dep_subst.lean | 4 ++-- tests/lean/run/t1.lean | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/lean/run/dep_subst.lean b/tests/lean/run/dep_subst.lean index 3e14134e5..bbba1bff4 100644 --- a/tests/lean/run/dep_subst.lean +++ b/tests/lean/run/dep_subst.lean @@ -10,7 +10,7 @@ begin exact finset.card fxs 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 induction fn₁ with fxs₁ h₁, induction fn₂ with fxs₂ h₂, @@ -18,7 +18,7 @@ begin apply sorry 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 induction fn₁ with fxs₁ h₁, induction fn₂ with fxs₂ h₂, diff --git a/tests/lean/run/t1.lean b/tests/lean/run/t1.lean index 8e8b6275e..3b8b79674 100644 --- a/tests/lean/run/t1.lean +++ b/tests/lean/run/t1.lean @@ -4,7 +4,7 @@ print raw ((Prop)) print raw Prop print raw fun (x y : Prop), x x 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 ∀ (x y : Prop) {z : Prop}, x print raw forall {x y : Prop} w {z : Prop}, x