idris-examples Some examples of programs with dependent types from Type Theory course in IFMO University. TODO Пары, алгебраические типы, экзистенциальные типы