DependentTypes


DependentTypes

DependentTypes Namespace

TypeDescription
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

ModuleDescription
Helpers

Inline helper functions for dependent types.

Fork me on GitHub