This is an old revision of the document!

A PCRE internal error occured. This might be caused by a faulty plugin

====== Rich Model Language ====== ===== Syntax ===== * lisp syntax based on Isabelle identifier names (perhaps clean-up names in Isabelle itself) * tools to provide nicer surface syntax and generate lisp syntax * we have a candidate using LR(1) parser (CUP) * an earlier version: [[Vepar Grammar]] ===== Semantics ===== Classical HOL * built in operators * define them whenever natural, or state strong enough properties ===== Type System ===== Simple types Parametric polymorphism ===== Starting Points ===== Document summarizing operators of interest: * {{:isabellemain.pdf|What's in Isabelle Main, October 14, 2009}} Some differences: * separate operators for + on integers, reals * no 'nat' for now, indexing lists gives unknown value for negative * 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 * a subset of list operations