Library MetaRocq.Quotation.ToTemplate.All
From MetaRocq.Common Require Import config.
From MetaRocq.Template Require Import Ast Typing.
From MetaRocq.Template Require WfAst TypingWf.
From MetaRocq.Quotation.ToTemplate.Template Require Ast Typing WfAst TypingWf.
Module Raw.
Definition quote_checker_flags : checker_flags → Ast.term := config.quote_checker_flags.
Definition quote_global_env_ext : global_env_ext → Ast.term := Ast.QuoteEnv.quote_global_env_ext.
Definition quote_context : context → Ast.term := Ast.QuoteEnv.quote_context.
Definition quote_term : Ast.term → Ast.term := Ast.quote_term.
Definition quote_typing {cf : checker_flags} {Σ Γ t T} : (Σ ;;; Γ |- t : T) → Ast.term := Typing.quote_typing.
Definition quote_red {Σ Γ x y} : @red Σ Γ x y → Ast.term := Typing.quote_red.
Definition quote_wf_local {cf : checker_flags} {Σ Γ} : wf_local Σ Γ → Ast.term := Typing.quote_wf_local.
Definition quote_wf {cf Σ} : @wf cf Σ → Ast.term := Typing.quote_wf.
Definition quote_wf_ext {cf Σ} : @wf_ext cf Σ → Ast.term := Typing.quote_wf_ext.
Module WfAst.
Definition quote_wf {Σ t} : @WfAst.wf Σ t → Ast.term := WfAst.quote_wf.
End WfAst.
From MetaRocq.Template Require Import Ast Typing.
From MetaRocq.Template Require WfAst TypingWf.
From MetaRocq.Quotation.ToTemplate.Template Require Ast Typing WfAst TypingWf.
Module Raw.
Definition quote_checker_flags : checker_flags → Ast.term := config.quote_checker_flags.
Definition quote_global_env_ext : global_env_ext → Ast.term := Ast.QuoteEnv.quote_global_env_ext.
Definition quote_context : context → Ast.term := Ast.QuoteEnv.quote_context.
Definition quote_term : Ast.term → Ast.term := Ast.quote_term.
Definition quote_typing {cf : checker_flags} {Σ Γ t T} : (Σ ;;; Γ |- t : T) → Ast.term := Typing.quote_typing.
Definition quote_red {Σ Γ x y} : @red Σ Γ x y → Ast.term := Typing.quote_red.
Definition quote_wf_local {cf : checker_flags} {Σ Γ} : wf_local Σ Γ → Ast.term := Typing.quote_wf_local.
Definition quote_wf {cf Σ} : @wf cf Σ → Ast.term := Typing.quote_wf.
Definition quote_wf_ext {cf Σ} : @wf_ext cf Σ → Ast.term := Typing.quote_wf_ext.
Module WfAst.
Definition quote_wf {Σ t} : @WfAst.wf Σ t → Ast.term := WfAst.quote_wf.
End WfAst.
N.B. Only works if you Import Raw.QuoteNotationHints
Notation quote := Init.quoted_term_of (only parsing).
Module QuoteNotationHints.
Export (hints) Quotation.ToTemplate.Init
Quotation.ToTemplate.Template.Ast
Quotation.ToTemplate.Template.Typing
Quotation.ToTemplate.Template.WfAst
Quotation.ToTemplate.Template.TypingWf
.
End QuoteNotationHints.
End Raw.
Module QuoteNotationHints.
Export (hints) Quotation.ToTemplate.Init
Quotation.ToTemplate.Template.Ast
Quotation.ToTemplate.Template.Typing
Quotation.ToTemplate.Template.WfAst
Quotation.ToTemplate.Template.TypingWf
.
End QuoteNotationHints.
End Raw.