Conversation

Good support for continuous editing should not require any explicit action from the user at all

Yeah the continuous editing in Lean is something I love so much! I love it how things live update as I do stuff, but maybe I’m just used to that from other languages… I generally use source control if I want to remember a past state.

You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more

Ahhh yeah that sounds like a massive pain

And yeah I'm really fascinated about how the benefits of both could somehow be accommodated. But I'm always wanting to have my cake and eat it and it constantly gets me into trouble hah.

I haven't checked the state of Lean 4 in a while but yeah last time I was using it I also missed (for example) the user-driven hole-based editing you get in Adga.

I'd actually love to see a demonstration of someone effectively using them. Anyone know of such a recording?

Not sure… I can't remember how I learned in the past… I know somehow along the line I learned how you could plonk stuff in the hole and then run a command to case split or proof search based on that stuff…? Been a while since I goofed about with Agda and am far from an expert.

Writing an Agda program interactively

I just searched on youtube and maybe this one?

youtube.com

We develop our first Agda program step by step by using the Agda emacs mode to interact with the type checker.

Replying to

and

It's just a intro tutorial though so probably not illustrative of more advanced cases. I also think I recall seeing people also being able to extend the hole commands with custom tactics as well, but not sure how common that is.

2:27 PM · Sep 2, 2022Twitter Web App

Replying to

and

But yeah, shows how you use the hole to direct splitting and refining the state of the program. So you end up sort of… pushing around holes in order to build up your program… uhh proof.