Maîtrise des types et fonctions en Idris

📋 Plan du Cours

1. Signature fonction Idris
2. Définition clause
3. Portée paramètre
4. Types de base Idris
5. Type Integer
6. Type Nat
7. Type Bool
8. Type String
9. Fonction show
10. Fonctions print et printLn
11. Type IO ()
12. Exécution REPL Idris

📖 1. Signature fonction Idris

🔑 Notions clés & Définitions

• Signature d’une fonction : La déclaration qui indique le nom de la fonction, ses types d’entrée et de sortie. Elle a la forme nom : Type1 -> Type2. Exemple : abs : Integer -> Integer.
• Définition d’une fonction : La mise en œuvre concrète de la fonction, sous la forme <motif> = <expression>. Exemple : abs x = if x < 0 then -x else x.
• Clause : Règle associée à une fonction, composée d’un motif (pattern) et d’une expression. Elle indique comment évaluer la fonction pour un motif donné.
• Portée d’un paramètre : La zone dans laquelle un paramètre est visible, généralement l’expression à droite du = où il est déclaré. Le paramètre n’est accessible qu’à cet endroit.
• Types de base en Idris : Types fondamentaux tels que Integer (entiers relatifs), Nat (entiers naturels), Bool (booléens), String (chaînes de caractères).
• Classe de type Show : Contrat indiquant qu’un type peut être converti en chaîne de caractères via la fonction show. Exemple : show : Show a => a -> String.

📝 Points essentiels