Unisciti al track Idris di Exercism per accedere a 58 esercizi con l'analisi automatica del codice e mentoring personale, tutto 100% gratuito.
module EvenOdd
data Even : Nat -> Type where
EZ : Even Z
ES : Even n -> Even (S (S n))
ee : Even n -> Even m -> Even (n + m)
ee EZ m = m
ee (ES n) m = ES (ee n m)
Migliora nella programmazione con esercizi divertenti e gratificanti che mettono alla prova la tua comprensione dei concetti su Exercism.
Determina se una frase usa tutte le lettere dell'alfabeto latino.
Aiuta a mettere in fila i clienti al Deli di Yaʻqūb.
Implementa il gioco della vita di Conway.
La sicurezza prima di tutto! Forti garanzie sulla correttezza dei programmi in fase di compilazione.
Ispirato al calcolo lambda, lo scope e i cicli si esprimono definendo e chiamando funzioni.
Raggruppare i tipi in classi offre un sovraccarico sicuro rispetto ai tipi.
L'immutabilità dei dati permette una concorrenza più sicura e su cui è più semplice ragionare.
Idris offre un piccolo numero di funzionalità di uso generale.
Idris è un banco di prova per la ricerca in costante sviluppo
Ogni linguaggio ha il suo modo di fare le cose. La traccia Idris non fa eccezione. I nostri mentori ti aiuteranno a imparare a pensare come uno sviluppatore Idris e a scrivere codice idiomatico in Idris. Dopo aver risolto un esercizio, invialo alla nostra squadra di volontari, che ti darà suggerimenti, idee e feedback su come renderlo più simile a quello che vedresti normalmente in Idris: ti aiuteranno a scoprire le cose che non sai di non sapere.
Scopri di più sul mentoringLa traccia Idris su Exercism ha 58 esercizi per aiutarti a scrivere codice migliore.
Vedi tutti gli esercizi di IdrisLa parte migliore: è gratis al 100% per tutti.
Unisciti alla traccia Idris