search

au-ts / cogent

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

improve Isabelle prettyprinter #394

Closed gteege closed 3 years ago

gteege commented 3 years ago

in cogent/isa-parser by adding syntactic sugar for let, if, and record update terms and provide some line breaks in terms

This makes specifically the shallow embedding much better readable for a human. Since only Isabelle syntactic sugar is added, this will not affect any proofs.

vjackson725 commented 3 years ago

These changes have been merged as of f0a14fb1