[[!redirects inductive-recursive type]] [[!redirects inductive recursive type]] < [[nlab:inductive-recursive type]] category:redirected to nlab