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. |