Ulf Norell
Ulf Norell
I suppose this is more of an Erlang Questions kind of topic, but I'm afraid I would get five people with incompatible answers each claiming that theirs is the obvious...
A function can have multiple specs, which [the documentation](http://erlang.org/doc/reference_manual/typespec.html#specifications-for-functions) calls overloading and whose semantics is intersection types. For instance, ```erlang -spec foo(boolean()) -> its_a_bool; (integer()) -> its_an_int. ``` means that...
See #4067. Causes some breakage in http://www.cse.chalmers.se/~nad/repos/equality/
Currently pattern synonyms accept implicit arguments, but not instance arguments. One use case for this would be to make an argument that's not an instance argument available for instance search....
Mimer fills the hole below with `zero ∷ []`, even though there is a constraint requiring the solution to sum to 3. ```agda open import Agda.Builtin.List open import Agda.Builtin.Nat open...
```haskell {-# LANGUAGE DataKinds #-} import Control.Monad.Freer import Control.Monad.Freer.Reader import Control.Monad.Freer.State import Data.Coerce badness :: Eff '[Reader (Int, Int)] a -> Eff '[State Int] a badness = coerce boom ::...
Spawned off from #1906. @vlopezj's example is here: [Issue_1906_branch.agda](https://gist.github.com/vlopezj/d3f51e5ba1941b527b801904eb271c9f). Swanky graph:  @andreasabel's observation: > Maybe we should never instantiateFull, but keep the meta-variables and their instantiations in the internal...
```agda module _ where open import Agda.Builtin.Reflection renaming (bindTC to _>>=_) open import Agda.Builtin.Unit open import Agda.Builtin.Nat hiding (_==_) open import Agda.Builtin.List open import Agda.Builtin.Equality Tactic = Term → TC...
To make contract inheritance (#198) more useful it might be nice to support parameterised contracts: ```sophia contract Parent(type t, x : t) = ... contract Main is Parent(int, 0) =...