Vuoi imparare e padroneggiare Idris?

Unisciti al track Idris di Exercism per accedere a 58 esercizi con l'analisi automatica del codice e mentoring personale, tutto 100% gratuito.

Informazioni su Idris

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)

58 esercizi di programmazione per Idris su Exercism. Da Pangramma a Il gioco della vita di Conway.


Migliora nella programmazione con esercizi divertenti e gratificanti che mettono alla prova la tua comprensione dei concetti su Exercism.

Vedi tutti gli esercizi di Idris su Exercism

Funzionalità principali di Idris


Idris

Tipi dipendenti

La sicurezza prima di tutto! Forti garanzie sulla correttezza dei programmi in fase di compilazione.

Puramente funzionale

Ispirato al calcolo lambda, lo scope e i cicli si esprimono definendo e chiamando funzioni.

Classi di tipi

Raggruppare i tipi in classi offre un sovraccarico sicuro rispetto ai tipi.

Multithread

L'immutabilità dei dati permette una concorrenza più sicura e su cui è più semplice ragionare.

Compatto

Idris offre un piccolo numero di funzionalità di uso generale.

Innovativo

Idris è un banco di prova per la ricerca in costante sviluppo

Ricevi mentoring nello stile di Idris

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 mentoring

Esercizi Idris creati dalla community

La traccia Idris su Exercism ha 58 esercizi per aiutarti a scrivere codice migliore.

Vedi tutti gli esercizi di Idris
Idris

Inizia con la traccia Idris

La parte migliore: è gratis al 100% per tutti.

Unisciti alla traccia Idris