Andre Knispel

Loss of context in `checkType` primitive

2

Consider this Agda code: ```agda module Tactic.Derive.Test where open import Agda.Builtin.Reflection open import Data.Product open import Data.List open import Data.Unit open import Data.Bool open import Data.Nat _>>=_ = bindTC data...

`scriptsNeeded` check in Dijkstra

5

I'll leave this here for documentation purposes: We don't want to do an equivalent of `scriptsNeeded` on subtransactions because it restricts potential optimization use cases. E.g. if we have lots...

Should simple scripts (i.e. Multisig/Timelock) be allowed in transactions containing subtransactions?

3

Since we can't have Plutus scripts of version 3 or eariler in transactions containing subtransactions (for various reasons - the most relevant to this question of them being that scripts...

The `Home` page of the new documentation is confusing

4

The `Home` page is just a copy of the `README` file. So when you land on it when looking for the actual specification you're naturally directed to this section: Clicking...

Since I'm thinking about it right now, here are some things that should help readability a bit: - `UTXO-inductive` should be renamed to `UTXO`. It's not an induction rule, so...

Here's some Agda code that takes exponential time to type check: ```agda module Test where open import Data.Bool open import Data.Product open import Function open import Relation.Binary.PropositionalEquality open import Relation.Nullary...