DependentTypes
DependentTypes Namespace
Type | Description |
DependentPair<'Sigma, 'Config, 'T, 'T2> |
'T -> 'T * 'T2 dependent pair |
DependentType<'Pi, 'Config, 'T, 'T2> |
'T -> 'T2 dependent type |
Pi<'Config, 'T, 'T2> |
Construction / validation type for DependentType |
Sigma<'Config, 'T, 'T2> |
Construction / validation type for DependentPair 'T -> 'T * 'T2 |
SomeDependentType<'Pi, 'Config, 'T, 'T2> |
'T -> 'T2 option dependent type |
Module | Description |
Helpers |
Inline helper functions for dependent types. |