rego-proofs.git - Lean proofs for my Master's thesis

Age	Commit message (Expand)	Author
2023-04-14	Proof-of-concept for identifier rewriting via walk API	Jakob L. Kreuze
2023-04-14	Beginning of generic AST walking and scope analysis	Jakob L. Kreuze
2023-04-14	Remove scope from AST	Jakob L. Kreuze
2023-04-14	Remove dead code	Jakob L. Kreuze
2023-04-13	Type inference now works on intermediate values in deref chain	Jakob L. Kreuze
2023-04-13	Context-aware type inference	Jakob L. Kreuze
2023-04-13	Form normalization	Jakob L. Kreuze
2023-04-13	Implementation of context->constraints	Jakob L. Kreuze
2023-04-13	Context-naÏve type inference	Jakob L. Kreuze
2023-04-13	checkpoint: Need to get around equality issue for (var ...) forms	Jakob L. Kreuze
2023-04-12	Beginning of programmatic constraint generation	Jakob L. Kreuze
2023-04-12	Sketch for type inference	Jakob L. Kreuze
2023-04-12	Compile examples/02-computable-assign-composite.rego	Jakob L. Kreuze
2023-04-12	Demonstrate compilation based on GOOPS approach	Jakob L. Kreuze
2023-04-12	Compile inductives	Jakob L. Kreuze
2023-04-12	Initial sketch for Lean code representation in Scheme	Jakob L. Kreuze
2023-04-12	Add examples/10-comprehensions	Jakob L. Kreuze
2023-04-11	Add exists-some type	Jakob L. Kreuze
2023-04-11	Add for-all type	Jakob L. Kreuze
2023-04-11	Comprehension types	Jakob L. Kreuze
2023-04-11	Allow rules to be marked as default	Jakob L. Kreuze
2023-04-08	Documentation of preprocess-policy and parse-policy interfaces	Jakob L. Kreuze
2023-04-07	Refactor compile-funcall using lenses	Jakob L. Kreuze
2023-04-06	Partially implement demangling	Jakob L. Kreuze
2023-04-06	Initial compile-funcall pass	Jakob L. Kreuze
2023-04-06	Use scope information in producing inductive predicate arguments	Jakob L. Kreuze
2023-04-06	Add `fresh-identifier'	Jakob L. Kreuze
2023-04-06	Add `extract-identifiers'	Jakob L. Kreuze
2023-04-06	Revert temporary fix that shouldn't have been committed	Jakob L. Kreuze
2023-04-06	`preprocess-policy' is correct for 06-complex-set-membership.rego	Jakob L. Kreuze
2023-04-06	Update interface to Rego.lean and update examples	Jakob L. Kreuze
2023-04-06	Refactor Rego.lean	Jakob L. Kreuze
2023-04-03	Update mathlib4	Jakob L. Kreuze
2023-04-03	Clean up root	Jakob L. Kreuze
2023-04-03	Complete move to AssocList	Jakob L. Kreuze
2023-04-03	Implement obj_eqv	Jakob L. Kreuze
2023-04-03	Initial idea of using AssocLists for representing objects	Jakob L. Kreuze
2023-04-02	Fix silent failure in parsing object literals	Jakob L. Kreuze
2023-04-02	Add compilation of object literals	Jakob L. Kreuze
2023-04-02	Include preprocess-policy stage	Jakob L. Kreuze
2023-04-02	Emit specification that works for 01-computable-assign-scalar	Jakob L. Kreuze
2023-03-31	Include set inclusion as a valid kind of head rule	Jakob L. Kreuze
2023-03-31	Parse lhs/rhs of head	Jakob L. Kreuze
2023-03-31	Initial parsing of rules	Jakob L. Kreuze
2023-03-31	Generalize 07-rule-with-dynamic-type	Jakob L. Kreuze
2023-03-31	Generalize 06-complex-set-membership	Jakob L. Kreuze
2023-03-31	Generalize 05-head-subset-rule	Jakob L. Kreuze
2023-03-31	Generalize 04-rule-free-variables	Jakob L. Kreuze
2023-03-31	Generalize 03-set-defined-by-predicate	Jakob L. Kreuze
2023-03-31	Non-constructive example for 01-computable-assign-scalar	Jakob L. Kreuze