¿Existe algún trabajo para crear un Marco de Teoría de Número Real / Probabilidad en COQ?
COQ es un probador de teoremas interactivo que utiliza el cálculo de construcciones inductivas, es decir, se basa en gran medida en tipos inductivos. Utilizándolos, las estructuras discretas como números naturales, números racionales, gráficos, gramáticas, semánticas, etc. se representan de manera...