Deputy: A Clojure-Hosted Dependently-Typed Language

Deputy is an experimental dependently-typed programming language embedded in Clojure, featuring inductive datatypes. It explores the implications of a Lisp-based REPL-driven workflow for both programming and type checking. Implemented as a Clojure library, it allows programmers to leverage the host language while working at the type level. This enables type-level computations that depend on values, unlocking powerful programming patterns. Importantly, despite the rich dynamic semantics of types, type checking remains a purely compile-time operation.