reformulate ITGround and ITExpand to use a "matched ground type" judgement
Closed this issue · 4 comments
see 2/5/18 version of notes in the #agda channel on slack
I used a judgemental syntax similar to the matching for arrows, since the vocabulary is similar and because the underbox-equals notation you have on paper is both way outside what unicode has to offer and hits one of Agda's few reserved glyphs.
can't use "floor" brackets?
I probably could. But it doesn't look much more like the paper syntax and would be a third unrelated overloading for ==, which is current 1) real actual equality and 2) mix-fix syntax that's part of the hole filling judgment for evaluation contexts. I kind of regret (2) for readability already and I don't think it's a good idea to add a third -- also using equals for things that happen to be relations but aren't equality is tacky anyway.
Ok.
Could encode it as a partial metafunction instead of a relation too.