New answers tagged

1

As mentioned by Andrej, this is an instance of transporting along an equivalence of families and display maps. In this specific case, we have an equivalence of graphs and relations. open import Function open import Data.Product open import Relation.Binary.PropositionalEquality open import Level renaming (zero to lzero; suc to lsuc) -- type of relations on a ...


4

OCaml and Scala are popular choices for types systems, but they are by no means the only languages you can write a compiler, interpreter, typechecker, or type system in. Type-checking involves traversing syntax trees representing terms and types. Languages with some form of algebraic data type make this easy, since these traversals can be defined using ...


Top 50 recent answers are included