redtt

redtt copied to clipboard

Strict Propositions

1

They will be available in Coq and agda, and if I understand things well they are consistent with CTT. Should we want them in redtt? https://github.com/coq/ceps/pull/37

spitters

favonia

favonia

favonia

What is missing from the current name printing?

8

0. Sometimes Name.pp is used and sometimes Pp.Env and Name.to_string are used. Needs to be consistent. 1. We are still shadowing global names in the signature (including constructors, data types,...

favonia

Consider adding a new class for volatile terms in addition to commands and constructors

5

This class includes the "contsructors" for `V` types, `fhcom` types, and maybe more in the future. One of the invariants is that a *volatile* term can always synthesize the most...

favonia

favonia

Expose generalize tactic to the user

2

The “generalize” tactic is useful. We should expose it to the user!

jonsterling

So much duplication! So much opportunity for bugs!

jonsterling

Avoid re-typechecking

1

0. Avoid expanding things unless necessary or otherwise too expensive. 1. Respect `opaque let`. @jonsterling

favonia