diff options
| author | Théo Zimmermann | 2019-01-25 19:13:12 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-01-25 19:13:12 +0100 |
| commit | 07be5ac6dcbaeb7dac4c38d6146d41d96e96da59 (patch) | |
| tree | caddde1938fdc88a4c2f32b91b78d5cc4608e49f | |
| parent | 2d19a8c0120fa66c771497303d38c12b69af5971 (diff) | |
| parent | 8d6d5e3107f2b5f075d7daca69eeaf5fbbd7d0f4 (diff) | |
Merge PR #9391: Clarify meaning of Primitive Projections
Reviewed-by: Zimmi48
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index d0e44cd212..50a56f1d51 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -234,7 +234,8 @@ Primitive Projections extended the Calculus of Inductive Constructions with a new binary term constructor `r.(p)` representing a primitive projection `p` applied to a record object `r` (i.e., primitive projections are always applied). - Even if the record type has parameters, these do not appear at + Even if the record type has parameters, these do not appear + in the internal representation of applications of the projection, considerably reducing the sizes of terms when manipulating parameterized records and type checking time. On the user level, primitive projections can be used as a replacement |