Brendan Zabarauskas on Twitter

This Tweet was deleted by the Tweet author. Learn more

Art Yerkes

@prozacchiwawa

Apr 12, 2020

Interested in seeing if there's a streamlined process for applying proof or writing tactics. I've slogged through a few proofs in idris, but it's quite tiring ... enough to where a little more pain on the implementation would be welcome if the prover was more flexible.

1

Replying to

and

Agda can do this: github.com/UlfNorell/agda - you can do similar stuff with elaborator reflection in Idris, but of course it's very handy to have support for this in the language's standard library.

6:06 PM · Apr 12, 2020Twitter Web App

Replying to

and

I've come close to starting agda as I find idris' elaborator code pretty incomprehensible yet. I like tactics (as in the old idris proof assistant) but haven't taken the time to learn enough agda to try making them.

1

Conversation