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

chore(tests/lean/run): fix tests

Browse source
This commit is contained in:
Leonardo de Moura 2016-10-03 21:44:48 -07:00
parent d549044d27
commit f9ca306fe2
2 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
tests/lean/run/fingerprint.lean
View file

@ -3,7 +3,7 @@ open tactic
run_command attribute.fingerprint `reducible >>= trace
definition ex0 : nat :=
by attribute.fingerprint `reducible >>= expr_of_nat >>= exact
by attribute.fingerprint `reducible >>= nat.to_expr >>= exact
attribute [reducible]
definition f : nat := 10
@ -11,7 +11,7 @@ definition f : nat := 10
run_command attribute.fingerprint `reducible >>= trace
definition ex1 : nat :=
by attribute.fingerprint `reducible >>= expr_of_nat >>= exact
by attribute.fingerprint `reducible >>= nat.to_expr >>= exact
vm_eval ex1
@ -20,7 +20,7 @@ definition g : nat := 20
run_command attribute.fingerprint `reducible >>= trace
definition ex2 : nat :=
by attribute.fingerprint `reducible >>= expr_of_nat >>= exact
by attribute.fingerprint `reducible >>= nat.to_expr >>= exact
vm_eval ex2
@ -30,7 +30,7 @@ rfl
definition h : nat := 20
definition ex3 : nat :=
by attribute.fingerprint `reducible >>= expr_of_nat >>= exact
by attribute.fingerprint `reducible >>= nat.to_expr >>= exact
example : ex1 = ex3 :=
rfl

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

@ -15,7 +15,7 @@ meta definition mk_defs : nat → command
| 0 := skip
| (n+1) := do
N ← to_expr `(nat),
v ← expr_of_nat n,
v ← n^.to_expr,
add_decl (declaration.defn (name.append_after `val n) [] N v reducibility_hints.opaque tt),
mk_defs n