6 lines
123 B
Text
6 lines
123 B
Text
open tactic
|
|
|
|
run_command do
|
|
e ← to_expr `(nat.add),
|
|
fn ← eval_expr (nat → nat → nat) e,
|
|
trace (fn 10 20)
|