Matthieu Sozeau

Some pygment declarations for MetaCoq commands

3

and Print/Print Assumptions.

Changes for 8.16

2

Comments welcome!

PCUIC PHOAS

1

This adds a variant of the syntax in Parametric Higher-Order Abstract Syntax, which can be combined with Coq's custom notation entries to get more readable reified terms.

This PR adds a new loop-checking algorithm to MetaCoq, which should allow to handle arbitrary universe constraints efficiently, e.g. `max (u + 1, v) = max (j, k+ 2)`. It...

Add a target to build doc using alectryon (on top of case-representation-closed)

Weak-head reduction is defined just like red1 without the congruence rules. To show a standardization theorem on it we'll need to show that it commutes with "internal" reduction that just...

Playing with QuickChick to write tests for MetaCoq's typechecker, substitution, lifting, potential translations etc... together with my guides Leonidas Lampropoulos and Benjamin C. Pierce.

Here's an idea: to check universe constraints in the checker, we first build the transitive closure of the graph, then we should get constant time comparisons. We could also use...