suzanne.soy/cur
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Comments on more reorg

Browse Source
This commit is contained in:
William J. Bowman 2015-10-01 00:05:21 -04:00
parent bb86e4fabc
commit 5d5ec00052
No known key found for this signature in database
GPG Key ID: DDD48D26958F0D1A
1 changed files with 8 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
curnel/redex-core.rkt
View File

@ -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