search

au-ts / cogent

Cogent Project
https://trustworthy.systems/projects/TS/cogent.pml
Other
158 stars 26 forks source link

Fix and improve shallow representation #390

Closed gteege closed 3 years ago

gteege commented 3 years ago

This pull request provides three features for the shallow embedding: 1) fix of issue #382 by adding a type specification to all invocations of polymorphic functions. 2) improve reuse of monomorphic type synonyms: Extend it to types containing builtin array types. 3) Initial partial support for reuse of polymorphic type synonyms. This is not perfect, but it works in many cases.

Features 2 and 3 only make the shallow embedding better readable for humans. In all three cases no proofs should be affected.

vjackson725 commented 3 years ago

These changes have been merged as of f0a14fb