Jasper Hugunin

Support Propositional Extensionality when combining --cubical and --prop

6

Proposal: Add `primGlueProp` which acts analogously to `primGlue` but for `Prop`. Because types in `Prop` are definitionally irrelevant, instead of an equivalence it can simply take a bi-implication. This would...

invalid trace on small example

1

Running `depqbf --dep-man=simple --trace=qrp --traditional-qcdcl test.qdimacs`, with `test.qdimacs` containing: ``` p cnf 3 2 e 1 0 a 2 0 e 3 0 1 2 3 0 -1 -3 0...

Closes #305 Just ran into this today. At an absolute minimum, the language definition and grammar should be available even in untrusted workspaces, but a quick look suggests that the...

Minor feature request. This was considered in #2288 and postponed. I have a use case for leaving out implicit fields even if metas for the implicit right-hand sides are added...