Now we don't need to have separate is-X and hX definitions, and our functions can take fewer arguments.
I removed the unfold has-hlevel over all the property definitions because I found it helpful to keep it folded while interactively developing the eliminator branches. It's nice to see your goal in terms of has-hlevel before it gets unfolded.
Now we don't need to have separate
is-XandhXdefinitions, and our functions can take fewer arguments. I removed theunfold has-hlevelover all the property definitions because I found it helpful to keep it folded while interactively developing the eliminator branches. It's nice to see your goal in terms ofhas-hlevelbefore it gets unfolded.