Systematic error type in NewQuote

RedPRL / redtt

"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory

Apache License 2.0

204 stars 12 forks source link

Closed jonsterling closed 4 years ago

favonia commented 5 years ago

Are we just repeating the same thing, or employing some Thought to structure the error reporting?