Jon Sterling
Jon Sterling
@kaonn I think you may be misunderstanding my comment --- the infeasible part is that this `split` function depends on about a half-hour's worth of other proofs, and it is...
I kind of don't even want to classify as bugs things which only appear in proofs that are much more complicated than what redtt is built to withstand (== anything...
@ecavallo Heh, I bet I forgot to deal with neutrals? Let me think about it.
Resolved by #230
Ahh, my fix didn't quite work. I'm disabling strict composition for now. I want to discuss it with the crew more to see if it can be recovered, but let...
Well, if we will re-open it, let me at least rename it.
@3abc I believe the issue has to do with the fact that we do not yet fully support partial application of an n-ary extension type. I would have to check...
(Just as a remark, this is not as simple as it sounds -- we still need to be able to evaluate to a whnf, in order to implement the typechecker!!...
What would be cool is if I could *first* evaluate without unfolding, and then tell the evaluator "OK, I want you to unfold this" etc., and just keep trying until...
(Then, the idea is that both the typechecker and the conversion checker/quotation would exploit this.)