Conversation

Just tried the Alfa proof editor (cse.chalmers.se/~hallgren/Alfa/) and now I'm wondering why structure editors stayed niche. Took me 5min to get faster at this than I am in Agda w/Emacs. I wish there was a web interface à la Hazel (hazelgrove.org), maybe I'll take a stab at it.

joomy

@vowelharmony

May 8, 2018

*mind blown gif* I never thought of indexed data types as a function that case splits the indexing arg and returns a different data type in each case! Then to use a value of an indexed data type, you would have to case on the indexing arg first! (Nat if you want to split a Vec)

Brendan Zabarauskas

@brendanzab

May 9, 2018

How did you manage to have multiple case clauses? I couldn't figure out how to split on parameters :/

joomy

@vowelharmony

May 9, 2018

For append: after the type signature I had `append a m n xs ys = ?12`, then I pressed c for case and said I wanted to split on m. Then I had what you see above. Then I pressed c again and said I wanted split on xs. So on and so forth. Did that help? What error are you getting?

Replying to

and

Yeah, I’ll try again later - just wasn’t clear to me. Doing the case thing was bringing up the case expression, rather than splitting the function into multiple clauses. Might have been splitting on the wrong thing

2:10 AM · May 9, 2018Twitter for iPhone

Replying to

and

Woo, I did a thing!

Still feels abit awkward/clunky to me, but it might be because it's just an older UI with non-standard conventions. But then, I found that with Hazel too. But still, super cool stuff! I've seen Alfa's cool looking screenshots before, but never thought to actually try it out.