diff options
| author | Marcos Magueta <maguetamarcos@gmail.com> | 2026-07-12 01:06:21 -0300 |
|---|---|---|
| committer | Marcos Magueta <maguetamarcos@gmail.com> | 2026-07-12 01:06:21 -0300 |
| commit | c3b4c7aee1f0d4beb078938d330e982e752927a1 (patch) | |
| tree | 49c2e7c3561415b6eefc16c3f0df33a757ef802c /README.org | |
| parent | 7aacf596d73cc74eb9af381a72723b50b4069e30 (diff) | |
| download | SOL-c3b4c7aee1f0d4beb078938d330e982e752927a1.tar.gz SOL-c3b4c7aee1f0d4beb078938d330e982e752927a1.zip | |
decision 14: no application in term position, spec example rewritten flat
Diffstat (limited to '')
| -rw-r--r-- | README.org | 5 |
1 files changed, 4 insertions, 1 deletions
@@ -70,7 +70,10 @@ It covers: with checkers verified in Rocq; - the catalog as ordinary queryable relations; - subtyping as proven relation inclusion, intensional relation - identity, and canonical representatives for quotient domains. + identity, and canonical representatives for quotient domains; +- applications as propositions everywhere: no relation application + in term position, statements about results written flat as + membership. ** Core Design Principles and Pipeline Specification |