Lean
Lean
Σχετικά με LeanΕξάσκηση

Θέλεις να μάθεις και να κατακτήσεις τη διαδρομή Lean;

Γίνε μέλος στη διαδρομή Lean του Exercism και απόκτησε πρόσβαση σε 100 ασκήσεις με αυτόματη ανάλυση του κώδικά σου και προσωπική καθοδήγηση, όλα 100% δωρεάν.

Γίνε μέλος στη διαδρομή Lean Εξερεύνησε τις ασκήσεις

Σχετικά με τη διαδρομή Lean

namespace HelloWorld

inductive World where
    | earth | mars

def hello (world : World) : String :=
    match world with
    | .earth => "Hello, Earth!"
    | .mars  => "Hi, Mars!"

end HelloWorld

100 ασκήσεις προγραμματισμού για τη διαδρομή Lean στο Exercism. Από την άσκηση Τρίγωνο ως την άσκηση Άθροισμα πολλαπλασίων.

Γίνε καλύτερος στον προγραμματισμό με διασκεδαστικές, ανταποδοτικές ασκήσεις προγραμματισμού στο Exercism, που ελέγχουν πόσο καλά κατανοείς τις έννοιες.

Τρίγωνο

Τρίγωνο

Προσδιόρισε αν ένα τρίγωνο είναι ισόπλευρο, ισοσκελές ή σκαληνό.

Δύο κουβάδες

Δύο κουβάδες

Με δεδομένους δύο κουβάδες διαφορετικού μεγέθους, δείξε πώς να μετρήσεις μια ακριβή ποσότητα λίτρων.

Άθροισμα πολλαπλασίων

Άθροισμα πολλαπλασίων

Με δεδομένο έναν αριθμό, βρες το άθροισμα όλων των πολλαπλασίων συγκεκριμένων αριθμών μέχρι τον αριθμό αυτό, χωρίς να τον συμπεριλαμβάνεις.

Δες όλες τις ασκήσεις της διαδρομής Lean στο Exercism

Βασικά χαρακτηριστικά της διαδρομής Lean

Lean

Καθαρά συναρτησιακή

Οι ντετερμινιστικές συναρτήσεις κάνουν τον κώδικα προβλέψιμο, συνθέσιμο και πιο κατανοητό.

Εξαρτημένοι τύποι

Όταν κωδικοποιείς τους κανόνες απευθείας στους τύπους, αυτοί γίνονται αυτοτεκμηριωμένοι και οι άκυρες καταστάσεις δεν μπορούν να αναπαρασταθούν.

Προγράμματα και αποδείξεις

Γράψε προγράμματα και απόδειξε την ορθότητά τους στην ίδια γλώσσα. Η προδιαγραφή είναι κώδικας.

Αποδεδειγμένη ορθότητα

Πήγαινε πέρα από το testing, αποδεικνύοντας μαθηματικά κρίσιμες ιδιότητες του κώδικά σου.

Κλάσεις τύπων

Η κατηγοριοποίηση των τύπων σε κλάσεις παρέχει ελαφριά και επεκτάσιμη αφαίρεση.

Ισχυρός μεταπρογραμματισμός

Ένα ισχυρό framework για macros και elaborators σου επιτρέπει να επεκτείνεις τη γλώσσα ώστε να ταιριάζει στο πεδίο σου.

Καθοδηγήσου με τον τρόπο της διαδρομής Lean

Κάθε γλώσσα έχει τον δικό της τρόπο να κάνει τα πράγματα. Η διαδρομή Lean δεν αποτελεί εξαίρεση. Οι μέντορές μας θα σε βοηθήσουν να μάθεις να σκέφτεσαι σαν προγραμματιστής Lean και να γράφεις ιδιωματικό κώδικα σε Lean. Μόλις λύσεις μια άσκηση, υποβάλε την στην εθελοντική μας ομάδα και θα σου δώσουν υποδείξεις, ιδέες και σχόλια για το πώς να τη φέρεις πιο κοντά σε αυτό που θα έβλεπες συνήθως σε Lean - θα σε βοηθήσουν να ανακαλύψεις όσα δεν ξέρεις ότι δεν ξέρεις.

Μάθε περισσότερα για την καθοδήγηση

Ασκήσεις Lean από την κοινότητα

Η διαδρομή Lean στο Exercism έχει 100 ασκήσεις για να σε βοηθήσει να γράφεις καλύτερο κώδικα.

Δες όλες τις ασκήσεις της διαδρομής Lean
Lean

Ξεκίνα με τη διαδρομή Lean

Και το καλύτερο: είναι 100% δωρεάν για όλους.

Γράψου στη διαδρομή Lean