A question about tactics

Alex R

unread,

Feb 28, 2012, 7:45:21 AM2/28/12

to Idris Programming Language

(Foreword: I'm new to tactics, so a general guide would be welcome,
and an Idris-specific one more-so)

From what I've gathered, (quite possibly erroneously), It is
impossible to add tactics to Idris without recompiling. Is that the
case? Am I missing something crucial?

Edwin Brady

unread,

Feb 28, 2012, 10:31:02 AM2/28/12

to idris...@googlegroups.com

You're not missing anything, unfortunately, at least at the moment. I do have in mind a DSL for tactic construction (like Coq's Ltac, only more typed) but I haven't implemented it yet.

I am planning to write up how tactics work, and how to make your own, pretty soon. I can't estimate reliably how long it'll take though...

Edwin.

Dominic Mulligan

unread,

Feb 28, 2012, 10:52:51 AM2/28/12

to Idris Programming Language

> I am planning to write up how tactics work, and how to make your own, pretty soon. I can't estimate reliably how long it'll take though...

I'd be interested in this. I tried implementing a "contradiction"
tactic last week but it wasn't clear to me the best way to go about it
when I started hacking, and it turned into a big mess. Do you have
any documentation at all on Idris' internals? Even simple things like
working out whether a hypothesis was an equality, or finding all the
constructors of a given inductive type, turned into surprisingly
involved tasks.

Dom

Alex Rozenshteyn

unread,

Feb 28, 2012, 10:57:46 AM2/28/12

to idris...@googlegroups.com

Thanks. Looking forward to it.

--
Alex R

Anthony de Almeida Lopes

unread,

Feb 28, 2012, 12:38:07 PM2/28/12

to idris...@googlegroups.com

2012/2/28 Alex Rozenshteyn <rpglo...@gmail.com>

Thanks. Looking forward to it.

ditto

Reply all

Reply to author

Forward