Leonardo de Moura
abf61be8f6
chore(library/tactic): remove imp_tac, it is not needed anymore
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-08 00:57:04 -08:00
Leonardo de Moura
048151487e
feat(kernel): use Pi as forall/implication
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-08 00:38:39 -08:00
Leonardo de Moura
4ba097a141
feat(frontends/lean): use lowercase commands, replace 'endscope' and 'endnamespace' with 'end'
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-05 13:06:36 -08:00
Leonardo de Moura
9f08156a73
feat(frontends/lean/parser): combine Echo and Show commands into the 'print' command
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-05 11:03:35 -08:00
Leonardo de Moura
ce1213a020
feat(frontends/lean): use '(* ... *)' instead of '(** ... **)' for script code blocks
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-05 10:32:47 -08:00
Leonardo de Moura
028a9bd9bd
feat(frontends/lean/scanner): use Lua style comments in Lean
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-05 08:53:27 -08:00
Leonardo de Moura
f1b97b18b4
refactor(frontends/lean/parser): tactic macros, and tactic Lua bindings
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-26 15:54:53 -08:00
Leonardo de Moura
0c059a9917
feat(library/tactic): use _tac suffix instead of _tactic like Isabelle
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-05 20:06:32 -08:00
Leonardo de Moura
98897b467d
feat(frontends/lean/parser): add support for Lua expression code blocks
...
In expression code blocks, we do not have to write a "return".
After this commit, the argument of an apply command is a Lua expression instead of a Lua block of code. That is, we can now write
apply (** REPEAT(ORELSE(imp_tactic, conj_tactic, conj_hyp_tactic, assumption_tactic)) **)
instead of
apply (** return REPEAT(ORELSE(imp_tactic, conj_tactic, conj_hyp_tactic, assumption_tactic)) **)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-29 10:21:24 -08:00
Leonardo de Moura
b3f87e2e4f
feat(library/tactic): make THEN, ORELSE, APPEND, PAR and INTERLEAVE nary combinators
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-28 22:11:07 -08:00
