au-ts / cogent

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

fix and improve tuples shallow embedding #395

Closed gteege closed 3 years ago

gteege commented 3 years ago

The non-tuples shallow embedding in ShallowShared and Shallow_Desugar is only modified by list prettyprinting and type synonym use, hence no other proof steps should be affected.