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.

For question about natural numbers $\Bbb N$, their properties and applications
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
with abstract syntax trees.
4 questions
4 questions
3 questions
3 questions
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)
3 questions
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)
3 questions
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…
3 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].
3 questions
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].
3 questions
3 questions
3 questions
Module generally refers to a logical subdivision of the whole program.
3 questions
when referencing the GitHub repository https://github.com/UniMath/UniMath.
3 questions
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.
3 questions
Questions on basic arithmetic involving numerical quantities only.
3 questions
with verification that can be either static or dynamic. For a narrower definitions use `static-verification` or `formal-verification`.
3 questions
for polymorphism that restrict the range of types that can be used in a particular case.
3 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)
3 questions
Interactive Development Environment (IDE). These are software applications used for writing and developing with programming languages and other structured grammars.
3 questions
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…
3 questions
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…
3 questions
Questions regarding software errors during the usage or development of Proof Assistants.
3 questions
Artificial intelligence that improves automatically through experience.
3 questions
Questions regarding syntactic substitutions should be tagged with this.
3 questions
when discussing the relative logical strength of axiom sets or foundations of theorem provers
3 questions
For questions seeking recommendations for online or offline resources about proof assistants
3 questions
for proof assistants that are generic, in that they allow a variety of logics to used with them
3 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.
3 questions
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.
3 questions
for the ISAR (Intelligible semi-automated reasoning) proof language in the Isabelle proof assistant.
3 questions
Normally a proof assistant is used to complete a proof. As a side effect source code may be generated.
3 questions
for questions related to how proof assistants accommodate mathematical notation and symbolism.
2 questions
Things related to η-convertibility, η-expansion, η-reduction, and their use in simplifying proofs.
2 questions
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).
2 questions
1 2
3
4 5
7