lean2/tests/lua/expr7.lua

local a   = Const("a")
local A   = Const("A")
local vec = Const("vec")
local T   = Const("T")
print(Pi({{A, Type}, {a, A}, {A, vec(A)}, {a, A}}, a))
local t = mk_pi("A", Type, mk_pi("a", Var(0), mk_pi("A", vec(Var(1)), mk_pi("a", Var(0), T(Var(0), Var(2))))))
print(t)
feat(kernel/formatter): add binding_body_fresh, let_body_fresh, and simplify formatter Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-05-17 19:30:03 +00:00			`local a = Const("a")`
			`local A = Const("A")`
			`local vec = Const("vec")`
			`local T = Const("T")`
			`print(Pi({{A, Type}, {a, A}, {A, vec(A)}, {a, A}}, a))`
			`local t = mk_pi("A", Type, mk_pi("a", Var(0), mk_pi("A", vec(Var(1)), mk_pi("a", Var(0), T(Var(0), Var(2))))))`
			`print(t)`
refactor(kernel): remove 'let'-expressions We simulate it in the following way: 1- An opaque 'let'-expressions (let x : t := v in b) is encoded as ((fun (x : t), b) v) We also use a macro (let-macro) to mark this pattern. Thus, the pretty-printer knows how to display it correctly. 2- Transparent 'let'-expressions are eagerly expanded by the parser. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-06-24 23:27:23 +00:00