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.
C'è un modo per ottenere la divisione della sintassi/dalla prima biblioteca senza definirlo io? – mushroom
Ho provato ma non ci sono riuscito ... Il sistema dei moduli può essere fastidioso quando si cerca di ottenere una notazione in ambito ... – Ptival