[Translucency] Remove "require" feature?

RedPRL / cooltt

😎TT

http://www.redprl.org/

Apache License 2.0

217 stars 16 forks source link

[Translucency] Remove "require" feature? #375

Closed jonsterling closed 2 years ago

jonsterling commented 2 years ago

This PR removes the require feature, which greatly simplifies the implementation. require seems unnecessary, as we can use a local unfolding inside the type.

This PR also adds user-friendly output for the #print command.

But I'm not merging this directly into that branch until I've discussed it with coauthors.

jonsterling commented 2 years ago

Discussed with Daniel, will merge