Library NbSteps.nb_steps
The custom inductive domain of ns and nsa
Definition of ns/nsa as structural fixpoints on the domain predicate
An eliminator for š¯”»ns which follows the program scheme of ns and nsa
This page has been generated by
coqdoc