Experimental OCaml backend for Agda

coq
agda
dependent-types

#1

agda-ocaml is an experimental backend for Agda, that uses the OCaml runtime.

Even though it is still experimental, one of the benefits it might have to OCaml programmers is that it allows programmers to effortlessly switch from the OCaml typesystem to Agda and dependent types and the opposite.