5
Czy istnieje funkcja przeprowadzania podziału euklidesowego na osobniki w standardowej bibliotece Coq? Nie mogłem go znaleźć. Jeśli go nie ma, to czy istnieje jakiś powód, matematycznie, że nie powinien istnieć?Podział euklidesowy na osobniki w coq
Powodem tego chcę, ponieważ próbuję podzielić listę na dwie mniejsze listy. Chciałbym jedną listę być w przybliżeniu o połowę mniejszy od drugiego, więc jestem obliczeniowej (długość xs)/2.
Czy istnieje sposób, aby uzyskać/rodzaj składni z pierwszej biblioteki bez definiowania go samodzielnie? – mushroom
Próbowałem, ale się nie udało ... System modułów może być denerwujący przy próbie uzyskania notacji w zakresie ... – Ptival