formrre

Pattern matching in do notation

1

HOL currently doesn't support the following inside `do-od` notation: ``` (SOME x)

I have found myself in a situation where thinking about operator precedence, while getting familiar with a new theory confuses me. It would be nice to have a set_trace option...

parsingComputeLib doesn't build

25

`parsingComputeLib` doesn't build under some very specific conditions anymore, Holmake in `compiler/parsing` fails with: `Don't know how to build necessary target(s): /home/user/cakeml/semantics/semanticsComputeLib.ui` This happened, because `semanticsComputeLib` was moved into `semantics/proofs`....

# Description Defines a general Isbell duality between presheaves and co-presheaves. Prose probably needs couple more passes. ## Checklist Before submitting a merge request, please check the items below: -...

Type checking takes very long with agda-categories

2

This is with Agda version 2.6.3-b499d12. I have a relatively short file ```agda {-# OPTIONS --allow-unsolved-metas #-} module adjunctionOfMorphisms where open import Categories.Category open import Categories.Functor renaming (id to idF)...