mirror of
https://github.com/polarity-lang/polarity.git
synced 2025-12-23 09:19:50 +00:00
13 lines
398 B
Text
13 lines
398 B
Text
/// The codata type of pairs defined by a first and second projection.
|
|
codata Pair(a b: Type) {
|
|
/// First projection on a pair.
|
|
Pair(a, b).fst(implicit a b: Type): a,
|
|
/// Second projection on a pair.
|
|
Pair(a, b).snd(implicit a b: Type): b,
|
|
}
|
|
|
|
/// Constructing an element of the pair type.
|
|
codef MkPair(a b: Type, x: a, y: b): Pair(a, b) {
|
|
.fst(_, _) => x,
|
|
.snd(_, _) => y,
|
|
}
|