michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(tests/lean/run): adjust test to changes in the library

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-15 13:27:18 -07:00
parent 5b7fb1f61a
commit 094459504b
9 changed files with 11 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/run/class1.lean
View file

@ -1,5 +1,5 @@
import standard import standard
using num pair using num prod
definition H : inhabited (Prop × num × (num → num)) := _ definition H : inhabited (Prop × num × (num → num)) := _

2
tests/lean/run/class2.lean
View file

@ -1,5 +1,5 @@
import standard import standard
using num pair using num prod
theorem H {A B : Type} (H1 : inhabited A) : inhabited (Prop × A × (B → num)) theorem H {A B : Type} (H1 : inhabited A) : inhabited (Prop × A × (B → num))
:= _ := _

2
tests/lean/run/class3.lean
View file

@ -1,5 +1,5 @@
import standard import standard
using num pair using num prod
section section
parameter {A : Type} parameter {A : Type}

2
tests/lean/run/class6.lean
View file

@ -1,5 +1,5 @@
import standard import standard
using pair using prod
inductive t1 : Type := inductive t1 : Type :=
| mk1 : t1 | mk1 : t1

6
tests/lean/run/class8.lean
View file

@ -1,5 +1,5 @@
import standard import standard
using num tactic pair using num tactic prod
inductive inh (A : Type) : Prop := inductive inh (A : Type) : Prop :=
| inh_intro : A -> inh A | inh_intro : A -> inh A
@ -18,8 +18,8 @@ theorem inh_bool [instance] : inh Prop
theorem inh_fun [instance] {A B : Type} (H : inh B) : inh (A → B) theorem inh_fun [instance] {A B : Type} (H : inh B) : inh (A → B)
:= inh_rec (λb, inh_intro (λa : A, b)) H := inh_rec (λb, inh_intro (λa : A, b)) H
theorem pair_inh [instance] {A : Type} {B : Type} (H1 : inh A) (H2 : inh B) : inh (pair A B) theorem pair_inh [instance] {A : Type} {B : Type} (H1 : inh A) (H2 : inh B) : inh (prod A B)
:= inh_elim H1 (λa, inh_elim H2 (λb, inh_intro (mk_pair a b))) := inh_elim H1 (λa, inh_elim H2 (λb, inh_intro (pair a b)))
definition assump := eassumption definition assump := eassumption
tactic_hint assump tactic_hint assump

2
tests/lean/run/congr_imp_bug.lean
View file

@ -3,7 +3,7 @@
--- Released under Apache 2.0 license as described in the file LICENSE. --- Released under Apache 2.0 license as described in the file LICENSE.
--- Author: Jeremy Avigad --- Author: Jeremy Avigad
---------------------------------------------------------------------------------------------------- ----------------------------------------------------------------------------------------------------
import logic.connectives.basic logic.connectives.function import logic.connectives.basic struc.function
using function using function
namespace congr namespace congr

2
tests/lean/run/elab_bug1.lean
View file

@ -4,7 +4,7 @@
--- Author: Jeremy Avigad --- Author: Jeremy Avigad
---------------------------------------------------------------------------------------------------- ----------------------------------------------------------------------------------------------------
import standard import standard struc.function
using function using function

2
tests/lean/run/fun.lean
View file

@ -1,4 +1,4 @@
import standard import standard struc.function
using function num bool using function num bool

2
tests/lean/run/ptst.lean
View file

@ -1,5 +1,5 @@
import standard import standard
using pair using prod
-- Test tuple notation -- Test tuple notation
check (3, false, 1, true) check (3, false, 1, true)