sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2018-06-19	Coq: library name update (as we did for Lem)	Brian Campbell

2018-06-18	Separate bitvector access/update from generic vector access in std prelude	Brian Campbell
	(necessary for backends where they're different) Coq uint/sint and related fixes
2018-06-18	Coq: update prompt monad wrt Lem	Brian Campbell

2018-06-13	Coq: library updates, informative type errors, fix type aliases	Brian Campbell
	(The last bit is to declare type aliases as Type so that Coq uses the type scope for notation, so * is prod, not multiplication).
2018-06-12	Coq: support for range type, along with related existential improvements	Brian Campbell
	Plus - Complete solver support for inequalities - Reduce exponentials in solver
2018-06-12	Coq: add more to library	Brian Campbell

2018-06-08	Coq: existential and constraint solving work	Brian Campbell
	- add existential unpacking for function arguments - add mechanism for using properties for existentially typed top-level values (useful for the typechecking tests) - support for length_list and In in Coq constraint solving
2018-06-08	Coq: some very basic existential support	Brian Campbell
	Only single variable in places, only packed at literals and variables, no unpacking
2018-05-25	Coq: fill in some built-ins	Brian Campbell
	vector_access is a bit hacky at the moment - it expects a constraint to be shown between the index and the list size, but we don't track list sizes in general
2018-05-24	Coq: solve more constraints	Brian Campbell

2018-05-24	Help launch coqide	Brian Campbell

2018-05-24	Import (rather hacky) Coq Sail libraries	Brian Campbell