Programming_Languages_Idris Winter 2021 CS 581 Resources http://docs.idris-lang.org/en/latest/tutorial/starting.html Main Concept: Dependent Type: http://docs.idris-lang.org/en/latest/tutorial/interp.html Implicit Parameter: "WITH": http://docs.idris-lang.org/en/latest/tutorial/views.html#with-and-proofs