mirror of
https://github.com/polarity-lang/polarity.git
synced 2025-12-23 09:19:50 +00:00
6 lines
143 B
Text
6 lines
143 B
Text
use "./fun.pol"
|
|
|
|
/// The dependent function type.
|
|
codata Pi(a: Type, p: a -> Type) {
|
|
Pi(a, p).dap(a: Type, p: a -> Type, x: a): p.ap(x),
|
|
}
|