------------------------------------------------------------------------------ -- Agda code for the course dependently typed functional -- languages - 2011-01 -- Course home page: -- http://www1.eafit.edu.co/asr/courses/dependently-typed-functional-languages/index.html ------------------------------------------------------------------------------ -- The code has been tested with Agda 2.6.0.1 and Standard -- Library 1.1. module README where -- Lectures open import Lecture.NonDependentTypes open import Lecture.PropositionsAsTypes open import Lecture.InductionRecursion open import Lecture.EquationalReasoning open import Lecture.AlgebraicStructures open import Lecture.LeibnizEquality open import Lecture.InductiveFamilies open import Lecture.ReasoningAboutPrograms open import Lecture.ReasoningAboutPrograms.InsertSort open import Lecture.GeneralRecursion