meow.rkt

(define-syntax (typed-axiom syn)
  (syntax-parse syn
    #:datum-literals (:)
    #:with c (format-id syn "constant:~a" #'name #:source #'name)
    #:with name- (format-id syn "~a-" #'name #:source #'name)
    [(_:id name:id : type)
     (define name-ls (parse-telescope-names #'type))
     (define type-ls (parse-telescope-types #'type))
     (define result (parse-telescope-result #'type))
     
     #`(begin
         (struct c (#,@name-ls) #:transparent #:reflection-name 'name)
         (define-syntax name (make-rename-transformer (assign-type #'name- #'type)))
         ; (define-syntax name (lambda (syn) (assign-type #'name- #'type)))
         (define- name- ((curry c)))]))
      
(begin-for-syntax
(define (parse-telescope-name type)
   (syntax-parse type
      [(Pi (x : t) telescope) ...]
      [result ....])))