Conversation

Some way to an interactive proof editor for focused natural deduction.

0:53

7.2K views

237

Gergő Érdi @ ICFP

@gergo_erdi

Oct 28, 2019

Would be nice to see the context, not just the goal.

Bob Atkey

@bentnib

Oct 28, 2019

I'm planning to add an "assumptions?" command, like Agda's show context thing.

Replying to

and

Could you perhaps have the context to the side, updating as you go?

1:28 PM · Oct 31, 2019Twitter Web App

Replying to

and

Maybe, I was hoping that the comments inserted would be enough to give context. I'm a bit wary of flashing up too much changing information as the focus moves.