Wrote an Idris EDSL for emitting PostScript programs with statically-known stack effects. https://gist.github.com/nvanderw/9729860 …
@nvanderw Yes, my second thought was that 'word' taking a required stack size might be better.
-
-
@edwinbrady That's a nice idea! -
@edwinbrady That made defining words really elegant: lineto : PostScript (S (S n)) -> PostScript n lineto = word "lineto"
End of conversation
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.