A tag is a keyword or label that categorizes your question with other, similar questions. Using the right tags makes it easier for others to find and answer your question.
Positivity is a common restriction when defining inductive types in type-theory based proof assistants.
with abstract syntax trees.
In a rewriting system, one specifies a set of rules that describe valid replacements of subformulae by other ones. (from nLab).
Unification is a technique used in the implementation of proof assistants for purposes including solving of metavariables and resolution of type classes.
For questions about proof irrelevant propositions and related annotations. Irrelevant types carry typechecking information which is erased at runtime.
when a Proof Assistant is relying on automation. The automation can be internal or external to the proof assistant. An typic external form of automation is an automatic theorem prover. Co…
eliminators are proof relevant eliminations.
ssreflect is a special set of tactics designed to enable small-scale reflection proof methodology in Coq proof assistant.
Computational complexity is a measure of the amount of time (computational steps) or space that it takes for an algorithm to solve a particular problem. Use this tag above the complexity of theorem pr…
Things related to η-convertibility, η-expansion, η-reduction, and their use in simplifying proofs.
In mathematics and mathematical logic, a metatheory is a mathematical theory about another mathematical theory. (Source: Wikipedia)
Converting from one form to another. Such as converting a proof from a logic based framework to a dependent type framework.
with verification that can be either static or dynamic. For a narrower definitions use `static-verification` or `formal-verification`.
for polymorphism that restrict the range of types that can be used in a particular case.
A tower of universes is cumulative if A:Ui implies A:Ui+1 (rather than, say, Lift(A):Ui+1). (from Homotopy Type Theory)
Interactive Development Environment (IDE). These are software applications used for writing and developing with programming languages and other structured grammars.
Questions regarding syntactic substitutions should be tagged with this.
for the principle of functional extensionality in logic and proofs which states that two functions are equal if their values are equal at every argument.
Normally a proof assistant is used to complete a proof. As a side effect source code may be generated.
for proof assistants that are generic, in that they allow a variety of logics to used with them
Per Martin-Löf‘s dependent type theory, also known as intuitionistic or constructive type theory, is a foundation for constructive mathematics notably using П-types, Σ-types, and W-types.
A normal form is expression that can no longer be reduced, typically in the lambda calculus. See also [weak-head-normal-form] and [normalization].
A system of formal logic is consistent if false is not deducible in the system. (from nLab).
In type theory, a type rule is an inference rule that describes how a type system assigns a type to a syntactic construction. These rules may be applied by the type system to determine if a program is…
A graph is a collection of vertices and edges; each edge links a pair of vertices, defining a relationship of incidence between vertices and edges. (from nLab)
Module generally refers to a logical subdivision of the whole program.
Reflection allows a program to inspect and modify its own source code, allowing greater flexibility.
In logic, double negation is the operation that takes P to ¬¬P, where ¬ is negation. In other words, double negation is the composite of negation with itself. (from nLab)
Broadly speaking, constructive mathematics is mathematics done without the principle of excluded middle, or other principles, such as the full axiom of choice, that imply it, hence without “non-constr…