• Plugin and Correctness
    • non_uniform: computes the number of non-uniform parameters in an inductive type (syntactic check)
    • helperGen: Find container and build the nesting function
    • implication: a small plugin to add the contraposition of implications as axiom
    • trans_inj_sur: This proof shows that PCUICToTemplate is injective
    • Modes: implementation of a flag system in MetaCoq
    • constructorList: a small plugin to derive a list of all constructors of an inductive type
    • nested_datatypes: examples for nested types for testing
    • addContainer: adds a container to the registered database (using the unary parametricity translation)
    • removeNonAug: Post-processing of unary parametricity translation to remove unneeded arguments
    • show: Skeleton to derive show instances for inductive types (unfinished)
    • standardNested: Register often used container types with helpful assumption and proof functions
    • interactive: A completely interactive command with variable amount of obligations
    • MetaCoqInductionPrinciples: a file to introduce notations and load other files
    • destruct_lemma: the plugin for induction principles
    • de_bruijn_print: a helper function to print de Bruijn indices in humanly-readable
    • typing: the correctness proof of the plugin
    • PCUICToTemplate: a translation from PCUIC syntax to TemplateCoq
    • PCUICToTemplateCorrectness: the correctness statement with typing preservation
  • Tests