aboutsummaryrefslogtreecommitdiff
path: root/src/Compilers
Commit message (Expand)AuthorAge
* Import prim token notations before using themGravatar Jason Gross2018-08-24
* Add Z.land, Z.lor bounds stuff to zutil, also split up ZUtilGravatar Jason Gross2018-08-23
* Try out stronger land, lor boundsGravatar Jason Gross2018-06-27
* Add specialize_all_ways, fix a proof in src/Compilers/Z/ArithmeticSimplifierI...Gravatar Jason Gross2018-06-26
* Split off ZRange lemmasGravatar Jason Gross2018-02-10
* minor updates needed to make it compile with bbvGravatar Samuel Gruetter2018-02-05
* Fix incorrect overridding of bool notationsGravatar Jason Gross2018-01-05
* Handle the fact that we haven't forbidden TWord 3Gravatar Jason Gross2018-01-05
* Remove TWord 3 based addcarryx, subborrowGravatar Jason Gross2018-01-05
* Print bool as uint8_tGravatar Jason Gross2018-01-05
* Add support for {addcarryx,subborrow}_u{25,26}Gravatar Jason Gross2018-01-02
* Update CNotationsGravatar Jason Gross2018-01-02
* Fix an argument order issueGravatar Jason Gross2017-11-17
* Add interpf_SmartVarfGravatar Jason Gross2017-11-17
* Make arguments of InterpLinearize more implicitGravatar Jason Gross2017-11-17
* Add Interp{ExprEta,Linearize}_indGravatar Jason Gross2017-11-17
* Add more constant notationsGravatar Jason Gross2017-11-14
* Update GeneralizeVar to ensure WfGravatar Jason Gross2017-11-13
* Add some convenience notations in Z.Syntax.EqualityGravatar Jason Gross2017-11-13
* Remove dead code for renaming bindersGravatar Jason Gross2017-11-13
* Make pipeline options more easily extensibleGravatar Jason Gross2017-11-13
* Reflow commentGravatar Jason Gross2017-11-13
* Remove slow "intros [a b]"Gravatar Jason Gross2017-11-13
* Add faster version of intros [a b] for reflective stuffGravatar Jason Gross2017-11-13
* Add more constant notationsGravatar Jason Gross2017-11-13
* More granularity in src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.vGravatar Jason Gross2017-11-13
* Split up reflective side condition tacticsGravatar Jason Gross2017-11-13
* Add InterpComposeGravatar Jason Gross2017-11-13
* Add more constant notationsGravatar Jason Gross2017-11-12
* Add more constant notationsGravatar Jason Gross2017-11-12
* Add more constant notationsGravatar Jason Gross2017-11-12
* Add more constant notationsGravatar Jason Gross2017-11-12
* add reflexivity to reify autosolveGravatar Jason Gross2017-11-12
* Also unfold tuple for reificationGravatar Jason Gross2017-11-11
* Handle more base types in Z.ReifyGravatar Jason Gross2017-11-10
* Add more fine-grained cmovnz notationsGravatar Jason Gross2017-11-10
* Handle tuples in reificationGravatar Jason Gross2017-11-10
* Add unfold_flat_interp_tupleGravatar Jason Gross2017-11-10
* Use match in flat_interp_{,un}tuple'Gravatar Jason Gross2017-11-10
* Make a reification packageGravatar Jason Gross2017-11-07
* Generalize extended version of IdWithAltGravatar Jason Gross2017-11-06
* Add IdWithAlt to ZExtendedGravatar Jason Gross2017-11-04
* Add Zsub to extended syntaxGravatar Jason Gross2017-11-03
* Add more constant notationsGravatar Jason Gross2017-11-03
* Add more constant notationsGravatar Jason Gross2017-11-03
* Add more constant notationsGravatar Jason Gross2017-11-03
* Fix error in generated C notationsGravatar Jason Gross2017-11-03
* Add preformatting for casts of mulxGravatar Jason Gross2017-11-03
* Add more constant notationsGravatar Jason Gross2017-11-03
* Add notations for mulx involving uint8_tGravatar Jason Gross2017-11-03