Frederik Hanghøj Iversen

Hoogling signatures with constraints

2

I think it would be a nice feature if hoogle could show results for signatures with matching types but additional constraints. Say I hoogle (a -> b) -> f a...

Rework sexp behaviour

2

`enh-ruby-mode` rebinds `C-M-f` to `enh-ruby-forward-sexp`. That key is bound to `forward-sexp` by default. Similarly `C-M-n` is rebound to `enh-ruby-end-of-block` in stead of `forward-list` etc.. This means that the behaviour is...

Parse error for Haskell sections

1

Consider the program: ``` main = print $ (`div` 2) 3 ``` If you put the cursor inside the brackets anywhere *except* on the first back-tick character and hit `C-M-u`...

Multiple ≃'s

2

`Cubical._≃_` is defined via `Σ`. `Cubical.Univalence._≃_` is congruent but defined via a record. What's the motivation? Would you mind it if I let `Cubical.Univalence` import and use the one defined...

I propose the repo should be named `cubical` rather than `cubical-demo`. See e.g.: https://help.github.com/articles/renaming-a-repository/

Use `set -e`

3

I believe you can use `set -e` rather rather than `|| exit 1` https://github.com/Saizan/cubical-demo/blob/f9f793cc925dcde1c84788a68eef5c53384627b7/test.sh#L1

FYI: https://github.com/agda/agda/pull/2521

Fix issue with selections in iframes.

18

Call `getSelection` on the document that is the `ownerDocument` of the element being modified. I regenerated the contents of `dist` by doing `gulp bundler` - hope this is the idea.