Pull request: add new operations for `IMP-`

wimmers / poly-reductions

Polynomial-time reductions in Isabelle/HOL

2 stars 13 forks source link

Pull request: add new operations for `IMP-` #30

Closed BilelGho closed 3 years ago

BilelGho commented 3 years ago

create new operations as mentioned in issue #29

BilelGho commented 3 years ago

@notiho I hope that'll do it. let me know. @mabdula @maxhaslbeck checking this theory I thought that we could use some syntactic sugar over here. But I don't know how to actually do it. What do you think? if you approve are there some resources about it ?

notiho commented 3 years ago

Yeah looks like what we want

mabdula commented 3 years ago

I think adding syntax could make things look nicer. Do you want an example of new syntax constructs in Isabelle?

BilelGho commented 3 years ago

@notiho @mabdula @maxhaslbeck any suggestions to improve the syntax? Please check the last commit. If it is okay then please approve the PR.