diff options
Diffstat (limited to 'README.org')
| -rw-r--r-- | README.org | 6 |
1 files changed, 5 insertions, 1 deletions
@@ -71,9 +71,13 @@ It covers: - the catalog as ordinary queryable relations; - subtyping as proven relation inclusion, intensional relation identity, and canonical representatives for quotient domains; +- OCaml for the implementation, Rocq for the proofs, extraction + binding the two; - applications as propositions everywhere: no relation application in term position, statements about results written flat as - membership. + membership; +- relation references as a term kind, written =#Name=: relations as + data for transitions, higher-order arguments, and the catalog. ** Core Design Principles and Pipeline Specification |