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.
For question about natural numbers $\Bbb N$, their properties and applications
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…
with abstract syntax trees.
A formal language is a collection of words over an alphabet, i.e. strings of symbols from the alphabet, according to certain rules. (from nLab)
Higher inductive types (HITs) are a generalization of inductive types to higher dimensions. HITs are generated inductively by elements of itself and its iterated identity types. (from nLab)
A W-type is a set or type which is defined inductively in a well-founded way based on a type of “constructors” and a type of “arities”, with one constructor having a certain canonical form. As such it…
A normal form is expression that can no longer be reduced, typically in the lambda calculus. See also [weak-head-normal-form] and [normalization].
Use for proof assistants or type theories featuring an equality type that has a reflection rule creating judgemental equalities out of them. See also [reflection].
Module generally refers to a logical subdivision of the whole program.
when referencing the GitHub repository https://github.com/UniMath/UniMath.
for floating point numbers as defined for use in a computer floating-point register. Do not use this tag for the mathematical concept of a floating point number.
Questions on basic arithmetic involving numerical quantities only.
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.
for the HOL Interactive Theorem Prover. Do not use this tag for other proof assistants in the HOL family such as HOL Light. For questions about higher order logic use the tag (higher-orde…
Backward proofs are a type of proofs and logical reasoning that start from the goal and then use a set of inference rules backwards to obtain a set of sub-goals. The end goal is proved if all its subg…
Questions regarding software errors during the usage or development of Proof Assistants.
Artificial intelligence that improves automatically through experience.
Questions regarding syntactic substitutions should be tagged with this.
when discussing the relative logical strength of axiom sets or foundations of theorem provers
For questions seeking recommendations for online or offline resources about proof assistants
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.
For questions specific to the proof assistant Metamath. Metamath is a tiny language that can express theorems in abstract mathematics, accompanied by proofs that can be verified by a computer program.
for the ISAR (Intelligible semi-automated reasoning) proof language in the Isabelle proof assistant.
Normally a proof assistant is used to complete a proof. As a side effect source code may be generated.
for questions related to how proof assistants accommodate mathematical notation and symbolism.
Things related to η-convertibility, η-expansion, η-reduction, and their use in simplifying proofs.
A bundle is said to be univalent if every other bundle is a pullback of it in at most one way (up to homotopy). (from nLab).