summaryrefslogtreecommitdiff
path: root/src/state.ml
AgeCommit message (Expand)Author
2018-07-27Make type annotations abstract in type_check.mliAlasdair Armstrong
2018-07-09Add some syntactic sugar for IsabelleThomas Bauereiss
2018-07-07Coq: precise generic vectorsBrian Campbell
2018-06-06Some work on improving error messagesAlasdair Armstrong
2018-05-18Make named theorem collections of state monad more fine-grainedThomas Bauereiss
2018-05-12Fix bug in handling of registers with option typeThomas Bauereiss
2018-05-09Generate initial register state recordThomas Bauereiss
2018-05-03Work in progress on the coq backendBrian Campbell
2018-04-18Add first draft of Isabelle library documentationThomas Bauereiss
2018-04-09Stop vector_typ_args_of from failing when order is a variableBrian Campbell
2018-03-07Make union types consistent in the ASTAlasdair Armstrong
2018-02-26Add/generate Isabelle lemmas about the monad liftingThomas Bauereiss
2018-02-22Some Lem/OCaml compatibility fixesBrian Campbell
2018-02-16Don't generate undefined functions for generated register typesThomas Bauereiss
2018-02-15Rebase state monad onto prompt monadThomas Bauereiss
2018-02-15Re-engineer prompt monad of Lem shallow embeddingThomas Bauereiss