• Home
• About Coq
• Get Coq
• Documentation
• Community

Library Continuations.FOUnify_cps.nat_complements

Library Continuations.FOUnify_cps.end_term_unif

• • • 3) si p0 < p+1, one applies the recurrence hypothesis H
    • 4) si p0 = p+1, one applies the recurrence hypothesis H1.

Library Continuations.FOUnify_cps.deb_term_unif

• • diffelnb is an inductive definition
  • The definition of DIFFELNB is recursive.

Library Continuations.FOUnify_cps.is_in_quasiterm_term_subst

Library Continuations.FOUnify_cps.nat_term_eq_quasiterm

Library Continuations.FOUnify_cps.listv_is_in_lv

Library Continuations.weight.tree_plus

Library Continuations.weight.Nxaccu_ex

Library Continuations.weight.tests

Library Continuations.weight.Nmxaccu_ex

Library Continuations.weight.decl_exc

Library Continuations.weight.Naccu_cc

Library Continuations.weight.tree

Library Continuations.weight.specif

Library Continuations.polycont.copy

Library Continuations.polycont.huffman

Library Continuations.polycont.Mx_defs

Library Continuations.polycont.copy_cheat

Library Continuations.cps.applytac

Library Continuations.cps.cps_Nx

Library Continuations.cps.cps_N

Library Continuations.cps.cps_Nmx

• webmaster
• xhtml valid
• CSS valid