| <clayrat> dckc-ho, rewrite doesn't work on case expressions, it's a known old bug | |
| <clayrat> https://github.com/idris-lang/Idris-dev/issues/4001 | |
| <clayrat> if you define lookup via `with` then that line in the proof is simply `rewrite decEqSelfIsYes {x=key} in Refl` |
| {-# LANGUAGE DeriveFunctor #-} | |
| newtype Fix f = Fix { unFix :: f (Fix f)} | |
| data IntListF a = | |
| Cons Int a | |
| | Nil | |
| deriving Functor | |
| type IntList = Fix IntListF |
| import collection.immutable.Map | |
| import scala.annotation.tailrec | |
| object Rho { | |
| // Inputs is the type that defines all of our "listeners" in a process. | |
| // They are uniquely identified by the Name being listened on, and a following process. | |
| // There is no need to store the bound name here, as the bound name will be replaced by an identifier | |
| // based on its position in a process. (Similar to a De Bruijn Index). Two inputs will be regarded as equivalent | |
| // if they only differ in the bound names (are alpha equivalent). |
| node_modules/ | |
| dist/ | |
| *~ |
Disclaimer 1: Type classes are great but they are not the right tool for every job. Enjoy some balance and balance to your balance.
Disclaimer 2: I should tidy this up but probably won’t.
Disclaimer 3: Yeah called it, better to be realistic.
Type classes are a language of their own, this is an attempt to document features and give a name to them.
| (* Syntax of Extensible Data Notation -- http://github.com/edn-format/edn | |
| See https://github.com/edn-format/edn/issues/56 | |
| This grammar is written in slightly extended version of Wirth Syntax | |
| Notation. A description is appended to the end of this document. *) | |
| (* start *) |
