max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: fix test

Browse source 
It was working for the wrong reasons
This commit is contained in:
Leonardo de Moura 2020-11-27 09:00:11 -08:00
parent fcc382df08
commit 93cc8a6403
1 changed files with 3 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
tests/lean/run/subst1.lean
View file

@ -1,4 +1,4 @@
--
set_option trace.Meta.Tactic.subst true
@ -14,13 +14,12 @@ theorem tst2 (x y z : Nat) : y = z → x = z + y → x = z + z := by
subst h2
exact rfl
def BV (n : Nat) : Type := Unit
def BV (n : Nat) : Type := { a : Array Bool // a.size = n }
theorem tst3 (n m : Nat) (v : BV n) (w : BV m) (h1 : n = m) (h2 : forall (v1 v2 : BV n), v1 = v2) : v = cast (congrArg BV h1) w := by
theorem tst3 (n m : Nat) (v : BV n) (w : BV m) (h1 : n = m) (h2 : forall (v1 v2 : BV n), v1 = v2) : v = cast (congrArg BV h1.symm) w := by
subst h1
apply h2
theorem tst4 (n m : Nat) (v : BV n) (w : BV m) (h1 : n = m) (h2 : forall (v1 v2 : BV n), v1 = v2) : v = cast (congrArg BV h1.symm) w := by
subst n
apply h2