bch29 / agda-holes Goto Github PK

Sorry that I sent this as an issue, since I don't know of other ways to contact you. Thank you for creating Agda.Holes! I am wondering whether it is still being maintained ?

I tried to use it with a newer version of Agda (2.6.1). I needed some small changes to get it to work, namely,

• quantify over Set levels in two places in Holes.Prelude;
• adding a pragma {-# NOINLINE ⌞_⌟ #-} in Holes.Term.

Afterwards the examples seem to work, but my own equational proof still didn't go through, for reasons I don't understand.

Anyway, are you still maintaining this library?

I think you have a very nice application of reflection in Agda here and was wondering what the status of this project is nowadays.

One issue you note in the Readme is that since this is a master's thesis project, you cannot accept contributions. If you've graduated by now, it might be good to update the Readme :)

Cheers,

Arjen