Stream: MetaCoq

Topic: PCUIC Quotation

view this post on Zulip Jason Gross (Apr 13 2023 at 08:05):

What should I be aiming to quote in PCUIC? I'm about to open a PR that provides

  Definition quote_term : PCUICAst.term -> PCUICAst.term := PCUICAst.quote_term.
  Definition quote_typing {cf : checker_flags} {Σ Γ t T} : (Σ ;;; Γ |- t : T) -> PCUICAst.term := PCUICTyping.quote_typing.
  Definition quote_red {Σ Γ x y} : @red Σ Γ x y -> PCUICAst.term := PCUICReduction.quote_red.
  Definition quote_wf_local {cf : checker_flags} {Σ Γ} : wf_local Σ Γ -> PCUICAst.term := PCUICTyping.quote_wf_local.
  Definition quote_wf {cf Σ} : @wf cf Σ -> PCUICAst.term := PCUICTyping.quote_wf.
  Definition quote_wf_ext {cf Σ} : @wf_ext cf Σ -> PCUICAst.term := PCUICTyping.quote_wf_ext.

I skipped most of the definitions in PCUICReduction, and there's a lot of other theory. I think this is probably enough for Lob's theorem (if I can prove that all of these are well-typed). Is there more that would be especially useful to have quotations for?

Last updated: Jul 23 2024 at 21:01 UTC