search

ggrov / tinker

Graph based proof strategy language
http://ggrov.github.io/tinker/
6 stars 0 forks source link

Simplify rtechn representation and enable arguments #8

Closed ggrov closed 10 years ago

ggrov commented 10 years ago

Something like this:

type arg = string * string list ; datatype atomic = Rule | ERule | FRule | Subst | SubstAsm | Tactic datatype EvalProp = Or | Orelse datatype appfn = Appf of (atomic * arg) list (* to allow multiple here ) | Nested of EvalProp ( or or orelse *) | Identity

datatype T = RTechn of { name : string, appf: appfn}

ggrov commented 10 years ago

should support variables if goal type allows it