HOL icon indicating copy to clipboard operation
HOL copied to clipboard
verified publisher icon HOL-Theorem-Prover

Adds mrec and interp combinators to itreeTauTheory

Open xdrr opened this issue 1 year ago • 4 comments

This change introduces the mrec and interp combinators to itreeTauTheory. The mrec combinator is used extensively in the Pancake itree semantics.

xdrr avatar Jun 28 '24 04:06 xdrr

It would be good if you could add a comment above the new material explaining the new constants and how they might be used. If you want to go wild, it would be nice to have a description of the itree theories in the DESCRIPTION manual...

mn200 avatar Jul 01 '24 01:07 mn200

don't forget the proofs about their properties too!

Plisp avatar Jul 02 '24 00:07 Plisp

Your PR is failing our source code tests. (Locally, you can replicate this by doing a build -t.)

In particular, material under src/ can't use Unicode characters (except for the 'magic' quotes “”‘’ and the lambda).

mn200 avatar Jul 02 '24 00:07 mn200

It seems that this PR also needs an approval to start the CI tests, as the contributor is new.

binghe avatar Jul 11 '24 01:07 binghe

Is this work going to get finished?

mn200 avatar May 26 '25 00:05 mn200

Closing as moribund.

mn200 avatar Jun 06 '25 00:06 mn200