From 5d5ec00052acf038e989c4e1e7e64ac84c3c5403 Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Thu, 1 Oct 2015 00:05:21 -0400 Subject: [PATCH] Comments on more reorg --- curnel/redex-core.rkt | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/curnel/redex-core.rkt b/curnel/redex-core.rkt index bd0917d..3eaef8d 100644 --- a/curnel/redex-core.rkt +++ b/curnel/redex-core.rkt @@ -343,6 +343,14 @@ [(Θ-ref (in-hole Θ (hole e)) 0) e] [(Θ-ref (in-hole Θ (hole e)) natural) (Θ-ref Θ ,(sub1 (term natural)))]) +;; TODO: The next 3 metafunctons are a mess. They should probably be organized like this: +;; Σ-elim-telescope : Σ x_D U -> Ξ +;; This one should do all the work currently done in DTR-Elim_D +;; Σ-methods-telescope : Σ x_D t_P -> Ξ +;; Σ-constructor-method-telescope : Σ x_D x_c t_P -> Ξ +;; Σ-constructor-inductive-telescope : Σ x_D x_c -> Ξ +;; Σ-constructor-inductive-hypotheses : Σ x_D x_c t_P -> Ξ + ;; Returns the inductive hypotheses required for eliminating the ;; inductively defined type x_D with motive t_P, where the telescope ;; Φ are the inductive arguments to a constructor for x_D