Lib service

I’ve bundled together the first group of epigram programs that may become part of some kind of standard library at some point. I’ve hacked together a little something to generate the dependency graph and a nice clickable interface. You may want to check it out. For now, it lives in a subdirectory of my homepage, but it should move to sneezy at some point.

Comments are very welcome. Note that I’ve gone through the .epi files in epigram/durham/examples, but I haven’t finished looking into ctm, txa, or Thorsten’s course work yet. Besides the library files, I’ve gathered the following examples so far:

  • DecEqNat.epi - decidability of equality on Nat
  • DecEqType.epi - decidability of equality on simple types
  • Lam.epi - untyped lambda calculus, substitutions on terms
  • PlusComm.epi - proof that plus commutes
  • TakeWhile.epi - the name says it all
  • Bounded.epi - the bounded view
  • Eval.epi - evaluation of simply typed lambda terms

You can find example X on www.cs.nott.ac.uk/~wss/EpiLib/Examples/X.epi.

The line between examples and library functions can be rather fuzzy. If you disagree with my choices, let me know. I’ve tried to limit the modules in the library to those that have a fairly high chance of being reused.

Any feedback would be very welcome. If things aren’t going the way you would like them too, let me know sooner rather than later.

2 Responses to “Lib service”

  1. Conor Says:

    Cool! We probably ought to do a bit of pruning and tidying, but at least you’ve got us to first base.

    There’s already an empty directory epigram/durham/lib which should probably be where library stuff ends up. Are you cvs enabled yet? I can’t remember if I did anything intelligent about library paths but I bet I didn’t. Probably should do, so that we can keep the library in one place and the examples in another.

  2. pwm Says:

    The Eq library should probably be changed to use the inbuilt equality

Leave a Reply