3 commits

Author	SHA1	Message	Date
Leonardo de Moura	7bb6ccc089	refactor(library/init/meta): qexpr ==> pexpr	2016-08-05 17:04:36 -07:00
Leonardo de Moura	7ddc3c72dd	fix(frontends/lean/elaborator, library/vm/vm_qexpr): add and handle as_is annotation	2016-07-31 20:49:53 -07:00
Leonardo de Moura	586baa4118	feat(library,frontends/lean): support for quoted expressions in the VM, compiler and frontend ... TODO: invoke elaborator at tactic.to_expr	2016-06-15 16:06:39 -07:00