 08 Nov, 2018 40 commits


MARCHE Claude authored
we add the val (=.) operator

 15 Jun, 2018 40 commits


Andrei Paskevich authored

Andrei Paskevich authored
For the previous behaviour (no import), write "use/clone T as T". This shortens the most used "use/clone import" to simply "use/clone".

 14 Jun, 2018 40 commits


Andrei Paskevich authored
Clone "with axiom ." or "with goal ." to change the default ("with lemma ." is also accepted, just in case).

 14 Feb, 2018 40 commits


Raphael RieuHelft authored

 16 Jan, 2018 40 commits


Raphael RieuHelft authored

 22 Dec, 2017 40 commits


Andrei Paskevich authored

 20 Dec, 2017 40 commits


Raphael RieuHelft authored
Added axiom to stdlib: from_int injectivity

 15 Dec, 2017 40 commits


Guillaume Melquiond authored

 22 May, 2017 40 commits


MARCHE Claude authored
The underlying Monoid does not need to be commutative, and is indeed not in example fibonacci.mlw

 19 Oct, 2016 40 commits


Clément Fumex authored

 07 Mar, 2016 40 commits


MARCHE Claude authored

MARCHE Claude authored

 16 Oct, 2015 40 commits


MARCHE Claude authored
for pi by the best possible bounds in doubleprecision IEEE754 floatingpoint numbers

 20 Aug, 2015 40 commits


Andrei Paskevich authored
except for modules/impset.mlw (because of Fset) and modules/mach/* (because of program cloning), the standard library now typechecks. This is still very much the work in progress. Many functions and predicates have still to be converted to "let function" and "let predicate". Here are some TODOs:  do not require the return type for "val predicate", "val lemma", etc.  do not require explicit variant for "let rec" if the code passes the termination check in Decl (see list.why)  what should become "val ghost function" and what should stay just "function" (see array.mlw, matrix.mlw, string.mlw, etc)?  some defined functions in algebra.why and relations.why had to be removed, so that they can be implemented with "let function" in int.mlw (since they are defined, they cannot be instantiated with letfunctions). This seems too restrictive. One way out would be to authorise instantiation of defined functions (with a VC).  should we keep the keyword "model"? reuse of "abstract" in types breaks syntax coloring ("abstract" requires closing "end" in programs but not in types; maybe we can drop that "end" again?).

 25 Mar, 2015 40 commits


MARCHE Claude authored

 24 Mar, 2015 40 commits


MARCHE Claude authored

 03 Sep, 2014 40 commits


Andrei Paskevich authored
 update Coq and Isabelle realizations (TODO: PVS)

 21 Aug, 2014 40 commits


Guillaume Melquiond authored

 20 Oct, 2012 40 commits


Andrei Paskevich authored
+ create AUTHORS file + fix the linking exception in LICENSE + update the "About" in IDE + remove the trailing whitespace + inflate my scores at Ohloh

 11 Sep, 2012 40 commits


MARCHE Claude authored

 03 Sep, 2012 40 commits


MARCHE Claude authored

Guillaume Melquiond authored
Remove the incorrect Coq realization of PowerReal.pow by Rpower, since the latter is only meaningfully defined for positive first arguments, e.g. Rpower (1) 3 = 1!

Guillaume Melquiond authored

 18 Jul, 2012 40 commits


Guillaume Melquiond authored

 18 May, 2012 40 commits


MARCHE Claude authored

 22 Apr, 2012 40 commits


Guillaume Melquiond authored

 19 Apr, 2012 40 commits


MARCHE Claude authored
{h ... }: html escape [ ... ] : Why3 code escape

MARCHE Claude authored

 21 Mar, 2012 40 commits


MARCHE Claude authored

MARCHE Claude authored

 06 Feb, 2012 40 commits


JeanChristophe Filliatre authored
note that 'function' is still allowed

 30 Nov, 2011 40 commits


MARCHE Claude authored

 29 Nov, 2011 40 commits


Guillaume Melquiond authored

 05 Sep, 2011 40 commits


MARCHE Claude authored

 04 Sep, 2011 40 commits


MARCHE Claude authored

 29 Jun, 2011 40 commits


Andrei Paskevich authored
 No more "and", "or", "implies", "iff", and "~". Use "/\", "\/", ">", "<>", and "not" instead.  No more "logic". Use "function" or "predicate".

 15 Dec, 2010 40 commits


MARCHE Claude authored

 26 Oct, 2010 40 commits


Andrei Paskevich authored

 19 Oct, 2010 40 commits


MARCHE Claude authored
