Jon Sterling comments

Results 198 comments of


                                            Jon Sterling

selectively bind arguments in a multi-lambda?

I think this is a sick idea. Maybe with a different notation.

Proposal to extend boundary-sensitive refinement to positive types

let’s talk more about the hit case. i think there may be a way to make it work, but it may be subtle.

An idea for abstract function interfaces

@RobertHarper That's a nice connection with the datatype interfaces, indeed!

📛 Symbol.pp -> Symbol.dump?

agreed Sent from my iPhone > On Jun 12, 2021, at 12:37 AM, favonia ***@***.***> wrote: > > > There is no real pretty-printing of symbols without an environment....

🚰 filler-of tactical?

So personally i kind of preferred the other approach from the other ticket, but with that said, i think this is a fine idea that we could implement.

🚰 filler-of tactical?

What seems quite broken about it is that you cannot easily tell, up to definitional equality, that something is actually an hcom and extract the composition problem from it. So...

Elim on a variable already in the context?

My first thought is to not support this directly until we have some sick tactics that can generalize the goal properly --- it is not enough to generalize the goal...

Serialization and imports

This seems to be done. Shall we close this ticket? @favonia

Add types for the "fiber of El at A under \phi"

I have thought about it some more and I am not certain that the pay-off is big enough to justify this ticket being implemented just now. I will continue to...

Let the user define an Open Modality

So, in order for this to be useful for my purposes, i also need to extend cooltt with a type of "definitional isomorphisms". I have to think a bit about...