search

gmalecha / template-coq

Reflection library for Coq
MIT License
12 stars 0 forks source link

Recovering the type of an axiom from its quoted form? #9

Closed JasonGross closed 9 years ago

JasonGross commented 9 years ago

The quoted form of a program seems to be missing the type of axioms (and possibly types of constants, too?). Is there a way to recover them? Where do the types live in the kernel?

Axiom foo : Type.
Quote Recursively Definition qfoo := foo.
Print qfoo. (* qfoo = 
Ast.PAxiom "Top.foo" (Ast.PIn (Ast.tConst "Top.foo"))
     : Ast.program *)
gmalecha commented 9 years ago

This is solved.

JasonGross commented 9 years ago

Thanks!