This is a fix for the formula from: https://en.xen.wiki/w/Color_notation#Converting_a_Ratio_to%2Ffrom_a_Color_Name. Adapted from a code comment I wrote in microtonal-utils/color.js.
Suppose we're converting an interval with stepspan S and magnitude M.
Our monzo is [a b c d e ...>, where a and b are unknown and c, d, e, ... are known.
Let X = stepspan([0 0 c d e ...>) = 16*c + 20*d + 24*e + ...
Y = magnitude([0 2(S-X) c d e ...>) = round((2(S-X) + c + d + e + ...) / 7)
| -- Adapted from: | |
| -- - https://github.com/agda/agda/blob/4a93aa6ffbcc55df5e4f65ecb4dc1d6215501a79/test/Fail/Issue3327.agda | |
| -- - https://github.com/dhall-lang/dhall-lang/issues/250 | |
| module Hurkens where | |
| import Prelude; | |
| -- This should not be allowed | |
| data Sort : sort 0 where { |
| {-# OPTIONS --cubical --safe #-} | |
| module Dedekind where | |
| open import Cubical.Foundations.Everything | |
| open import Cubical.Data.Sigma | |
| open import Cubical.Data.Nat as Nat | |
| open import Cubical.Data.Bool as Bool | |
| elimBool : ∀ {ℓ} {P : Bool → Type ℓ} (a0 : P true) (a1 : P false) |