Jack Ek
Jack Ek
Would be useful with product types with named factors, or records, or whatever we want to call them.
macOS 10.13.4 nix 2.1.3 Output: ``` ➜ typedefs git:(master) nix-build default.nix -A typedefs these derivations will be built: /nix/store/chwyrvnnh59ib11crq31d0nfr6qiqmkn-idris-typedefs-dev.drv building '/nix/store/chwyrvnnh59ib11crq31d0nfr6qiqmkn-idris-typedefs-dev.drv'... unpacking sources unpacking source archive /nix/store/pqwi1h8976g6l8nab0hjnklywinl24w3-typedefs source root is...
Do we want to compare on literate strings, on generated `Doc`s, do we want to send the thing to the compiler in question, do there exist other options? As per...
Because of the type of `TMu : Vect k (Name, TDef (S n)) -> TDef n`, backends that can only handle closed terms run into issues when recursing into a...
As per the discussion here: https://github.com/typedefs/typedefs/pull/87#discussion_r243347434 My thinking is that it can allow us to make sure that the generated source code actually uses type variables that are in scope....
To polish the modules' interfaces.
This was already addressed in #81 and implemented in #85 and #87, but as of #109, it is broken and everything related to it has been commented out. ## Desired...
Steps to reproduce: 1. Go to https://deltabalances.github.io/trades.html#0x694e929bc5d2cdb66183a874bd19cfd2a7edcb08 and fetch data for Ethfinex for the single block `7436018`. 2. Compare the amount `10.000` in the single output entry to the amount...
This may be cleaner because it allows us to infer names purely based on a storage item. On the other hand, it makes location extraction for name generation more difficult,...