# Tags

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.
6 questions
with abstract syntax trees.
6 questions
In a rewriting system, one specifies a set of rules that describe valid replacements of subformulae by other ones. (from nLab).
6 questions
Unification is a technique used in the implementation of proof assistants for purposes including solving of metavariables and resolution of type classes.
6 questions
For questions about proof irrelevant propositions and related annotations. Irrelevant types carry typechecking information which is erased at runtime.
6 questions
6 questions
5 questions
5 questions
5 questions
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…
5 questions
eliminators are proof relevant eliminations.
5 questions
ssreflect is a special set of tactics designed to enable small-scale reflection proof methodology in Coq proof assistant.
5 questions
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…
5 questions
Things related to η-convertibility, η-expansion, η-reduction, and their use in simplifying proofs.
5 questions
In mathematics and mathematical logic, a metatheory is a mathematical theory about another mathematical theory. (Source: Wikipedia)
5 questions
Converting from one form to another. Such as converting a proof from a logic based framework to a dependent type framework.
5 questions
with verification that can be either static or dynamic. For a narrower definitions use static-verification or formal-verification.
4 questions
for polymorphism that restrict the range of types that can be used in a particular case.
4 questions
A tower of universes is cumulative if A:Ui implies A:Ui+1 (rather than, say, Lift(A):Ui+1). (from Homotopy Type Theory)
4 questions
Interactive Development Environment (IDE). These are software applications used for writing and developing with programming languages and other structured grammars.
4 questions
Questions regarding syntactic substitutions should be tagged with this.
4 questions
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.
4 questions
Normally a proof assistant is used to complete a proof. As a side effect source code may be generated.
4 questions
for proof assistants that are generic, in that they allow a variety of logics to used with them
4 questions
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.
4 questions
A normal form is expression that can no longer be reduced, typically in the lambda calculus. See also [weak-head-normal-form] and [normalization].
4 questions
4 questions
A system of formal logic is consistent if false is not deducible in the system. (from nLab).
4 questions
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…
4 questions
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)
4 questions
Module generally refers to a logical subdivision of the whole program.
4 questions
4 questions
4 questions
Reflection allows a program to inspect and modify its own source code, allowing greater flexibility.
3 questions
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)
3 questions
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…
3 questions