Differences
This shows you the differences between two versions of the page.
Next revision | Previous revision Next revision Both sides next revision | ||
rml [2009/10/08 21:41] vkuncak created |
rml [2009/10/14 16:01] vkuncak |
||
---|---|---|---|
Line 1: | Line 1: | ||
====== Rich Model Language ====== | ====== Rich Model Language ====== | ||
- | * http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle/doc/main.pdf | + | Tool chain |
+ | * lisp syntax based on Isabelle identifier names (perhaps clean-up names in Isabelle itself) | ||
+ | * tools to provide nicer surface syntax and generate lisp syntax | ||
+ | |||
+ | Document summarizing operators of interest: | ||
+ | * {{:isabellemain.pdf|What's in Isabelle Main, October 14}} | ||
+ | |||
+ | Some differences: | ||
+ | * separate operators for + on integers, reals | ||
+ | * no 'nat' for now, indexing lists gives unknown value | ||
+ | * a 'finite' predicate, no separate type | ||
+ | * introduce a type for SMT-LIB 2.0 (same problem for maps) | ||
+ | * finiteness inference | ||
+ | * no set intervals | ||
+ | * option types | ||
+ | * subset of list operations | ||