Grah, mysterious coverage error. I have a theorem that…: jcreed

Log in

No account? Create an account

Remember me

: Jason (jcreed) wrote,
2005-12-23 23:32:00

Jason
jcreed
2005-12-23 23:32:00

Grah, mysterious coverage error. I have a theorem that coverage-checks when I have a "hole" term at the type the theorem is supposed to output. The theorem consists of two mutually recursive statements A and B. If I add clauses to A (hoping to eventually remove the "hole" cases), then there are new missing cases reported for B. Insane!

---

ETA: Have found a way around it this time... the solution unfortunately isn't that general.

Tags: twelf, work

(no subject)

A paper on describing circuits in an agda DSL: http://www.staff.science.uu.nl/~swier004/publications/2015-types-draft.pdf
(no subject)

Going more carefully now through this little tutorial on fpga programming with the iCEstick. It's in spanish, which makes it slightly more…
(no subject)

Some further progress cleaning up the https://xkcd.com/1360/ -esque augean stables that is my hard drive. Tomato chicken I made a couple days ago…

Post a new comment
3 comments

Log in

(no subject)

(no subject)

(no subject)

Error