lean4-htt/tests/lean/run/meta_expr1.lean
2016-06-05 21:13:00 -07:00

4 lines
116 B
Text

import meta
open unsigned list
vm_eval expr.app (expr.app (expr.const "f" []) (expr.mk_var 1)) (expr.const "a" [])