2012-12-10 5 views
5

Esiste una funzione per eseguire la divisione euclidea sui naturali nella libreria standard Coq? Non sono riuscito a trovarne uno. Se non ce n'è uno, c'è una ragione, matematicamente, che non dovrebbe essercene uno?Divisione euclidea sui naturali in coq

La ragione per cui voglio questo è perché sto cercando di dividere una lista in due liste più piccole. Vorrei una lista in circa la metà delle dimensioni degli altri, in modo da sto Computing (lunghezza xs)/2.

risposta

2
+0

C'è un modo per ottenere la divisione della sintassi/dalla prima biblioteca senza definirlo io? – mushroom

+0

Ho provato ma non ci sono riuscito ... Il sistema dei moduli può essere fastidioso quando si cerca di ottenere una notazione in ambito ... – Ptival