rhiannon morris
bf605486f0
- misc.All doesn't need to be a ★¹ - add pair.map-fst and pair.map-snd - add bool.dup! - tweak quantities in eta.from-false - add fail.quox to all.quox - add qty.quox
73 lines
2 KiB
Text
73 lines
2 KiB
Text
def0 Qty : ★ = {"zero", one, any}
|
||
|
||
def dup : Qty → [ω.Qty] =
|
||
λ π ⇒ case π return [ω.Qty] of {
|
||
'zero ⇒ ['zero];
|
||
'one ⇒ ['one];
|
||
'any ⇒ ['any];
|
||
}
|
||
|
||
def drop : 0.(A : ★) → Qty → A → A =
|
||
λ A π x ⇒ case π return A of {
|
||
'zero ⇒ x;
|
||
'one ⇒ x;
|
||
'any ⇒ x;
|
||
}
|
||
|
||
def if-zero : 0.(A : ★) → Qty → ω.A → ω.A → A =
|
||
λ A π z nz ⇒
|
||
case π return A of { 'zero ⇒ z; 'one ⇒ nz; 'any ⇒ nz }
|
||
|
||
def plus : Qty → Qty → Qty =
|
||
λ π ρ ⇒
|
||
case π return Qty of {
|
||
'zero ⇒ ρ;
|
||
'one ⇒ if-zero Qty ρ 'one 'any;
|
||
'any ⇒ drop Qty ρ 'any;
|
||
}
|
||
|
||
def times : Qty → Qty → Qty =
|
||
λ π ρ ⇒
|
||
case π return Qty of {
|
||
'zero ⇒ drop Qty ρ 'zero;
|
||
'one ⇒ ρ;
|
||
'any ⇒ if-zero Qty ρ 'zero 'any;
|
||
}
|
||
|
||
def0 FUN : Qty → (A : ★) → (A → ★) → ★ =
|
||
λ π A B ⇒
|
||
case π return ★ of {
|
||
'zero ⇒ 0.(x : A) → B x;
|
||
'one ⇒ 1.(x : A) → B x;
|
||
'any ⇒ ω.(x : A) → B x;
|
||
}
|
||
|
||
def0 Fun : Qty → ★ → ★ → ★ =
|
||
λ π A B ⇒ FUN π A (λ _ ⇒ B)
|
||
|
||
def0 Box : Qty → ★ → ★ =
|
||
λ π A ⇒
|
||
case π return ★ of {
|
||
'zero ⇒ [0.A];
|
||
'one ⇒ [1.A];
|
||
'any ⇒ [ω.A];
|
||
}
|
||
|
||
def0 unbox : (π : Qty) → (A : ★) → Box π A → A =
|
||
λ π A ⇒
|
||
case π return π' ⇒ Box π' A → A of {
|
||
'zero ⇒ λ x ⇒ case x return A of { [x] ⇒ x };
|
||
'one ⇒ λ x ⇒ case x return A of { [x] ⇒ x };
|
||
'any ⇒ λ x ⇒ case x return A of { [x] ⇒ x };
|
||
}
|
||
|
||
def apply : (π : Qty) → 0.(A : ★) → 0.(B : A → ★) →
|
||
FUN π A B → (x : Box π A) → B (unbox π A x) =
|
||
λ π A B ⇒
|
||
case π
|
||
return π' ⇒ FUN π' A B → (x : Box π' A) → B (unbox π' A x)
|
||
of {
|
||
'zero ⇒ λ f x ⇒ case x return x' ⇒ B (unbox 'zero A x') of { [x] ⇒ f x };
|
||
'one ⇒ λ f x ⇒ case x return x' ⇒ B (unbox 'one A x') of { [x] ⇒ f x };
|
||
'any ⇒ λ f x ⇒ case x return x' ⇒ B (unbox 'any A x') of { [x] ⇒ f x };
|
||
}
|