fix(tests/lean): adjust tests to reflect recent changes
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
87da23649b
commit
419fb7464e
6 changed files with 0 additions and 7 deletions
|
@ -1,4 +1,3 @@
|
|||
import heq
|
||||
import macros
|
||||
import tactic
|
||||
|
||||
|
@ -7,4 +6,3 @@ theorem my_proof_irrel {a b : Bool} (H1 : a) (H2 : b) : H1 == H2
|
|||
H1_eq_H1b : H1 == H1b := hsymm (cast_heq (by simp) H1),
|
||||
H1b_eq_H2 : H1b == H2 := to_heq (proof_irrel H1b H2)
|
||||
in htrans H1_eq_H1b H1b_eq_H2
|
||||
|
||||
|
|
|
@ -1,6 +1,5 @@
|
|||
Set: pp::colors
|
||||
Set: pp::unicode
|
||||
Imported 'heq'
|
||||
Imported 'macros'
|
||||
Imported 'tactic'
|
||||
Proved: my_proof_irrel
|
||||
|
|
|
@ -1,4 +1,3 @@
|
|||
import heq
|
||||
variable Vector : Nat -> Type
|
||||
variable n : Nat
|
||||
variable v1 : Vector n
|
||||
|
|
|
@ -1,6 +1,5 @@
|
|||
Set: pp::colors
|
||||
Set: pp::unicode
|
||||
Imported 'heq'
|
||||
Assumed: Vector
|
||||
Assumed: n
|
||||
Assumed: v1
|
||||
|
|
|
@ -1,4 +1,3 @@
|
|||
import heq
|
||||
rewrite_set simple
|
||||
|
||||
set_option pp::implicit true
|
||||
|
|
|
@ -1,6 +1,5 @@
|
|||
Set: pp::colors
|
||||
Set: pp::unicode
|
||||
Imported 'heq'
|
||||
Set: lean::pp::implicit
|
||||
Assumed: g
|
||||
Assumed: B
|
||||
|
|
Loading…
Reference in a new issue