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.

The notion of abelian category is an abstraction of basic properties of the category Ab of abelian groups, more generally of the category RMod of modules over some ring, and still more generally of ca…
1 question
with abstract syntax trees.
7 questions
2 questions
1 question
For questions regarding Agda: the programming language / proof assistant.
61 questions
Two common classes of algebraic types are product types (i.e., tuples and records) and sum types (i.e., tagged or disjoint unions, coproduct types or variant types). (from Wikipedia)
2 questions
α-equivalence is used for renaming bound variables.
2 questions
In mathematics, analysis usually refers to any of a broad family of fields that deals with a general theory of limits in the sense of convergence of sequences (or more generally of nets), particularly…
1 question
1 question
when the question is about using a Proof Assistant for a purpose, how would you apply the Proof Assistant to solve a particular problem. Do not use this tag if it relates to a software ap…
11 questions
Arend is a theorem prover based on Homotopy Type Theory. It natively supports higher inductive types and a version of cubical syntax. IntelliJ Arend is a plugin for IntelliJ IDEA that turns it into a …
1 question
Questions on basic arithmetic involving numerical quantities only.
3 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
For questions regarding ATP's (Automatic Theorem Provers), which attempt to prove a theorem without any assistance. If you are using a Proof Assistant or an interactive theorem prover and are providin…
16 questions
when no human intervention is needed. If the questions concerns automated theorem proving use the tag automated-theorem-proving.
2 questions
for questions about whether an assertion can be accepted by the proof assistant without adding the axioms. This can be used in situations where it is not desired that the implementation o…
2 questions
An important and fundamental axiom in set theory sometimes called Zermelo's axiom of choice. It was formulated by Zermelo in 1904 and states that, given any set of mutually disjoint nonempty sets, the…
9 questions
An axiom is a proposition in logic that a given theory requires to be true: every model of the theory is required to make the axiom hold true. The sense however is that an axiom is a basic true propos…
1 question
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…
4 questions
Questions asked by a beginner user of proof assistants. We make an effort to be extra kind to such users.
73 questions
Bidirectional typing combines two modes of typing: type checking, which checks that a program satisfies a known type, and type synthesis, which determines a type from the program.
2 questions
Questions designed to generate a "big list" of certain results, examples, conjectures, etc. via many individual answers, each contributing one or a few instances. If the question is not objective con…
2 questions
Questions regarding binders (eg. by means of De Bruijn indices, HOAS, nominal approach) should be tagged with this.
6 questions
Bound variables refer to variables that serve as a placeholder to point to a binder. In calculus, "∫ t dx" is a binder and any free appearance of the variable "x" in "t" is bound.
1 question
A software bug is an error, flaw or fault in a computer program or system that causes it to produce an incorrect or unexpected result, or to behave in unintended ways.
3 questions
The process of converting source code files into standalone software artifact(s) that can be run on a computer.
1 question
For questions about using proof assistants to prove (integral and differential) calculus theorems. Do not use for lambda calculus, etc.
2 questions
Calculus of (co)Inductive Constructions is a pure type system (Coquand, Huet) equipped with addition types: arbitrary (co)inductive types implementing general (co)inductive schemes; universes as a cu…
13 questions
A type theory satisfies canonicity if every term computes to a canonical form, built explicitly using the constructors of its type.
7 questions
Categories are structures containing objects and arrows between them. Many mathematical structures can be viewed as objects of a category, with structure preserving morphisms as arrows. Reformulating …
22 questions
1 question
Checking is a way of examining to test accuracy, quality, or satisfactory condition of a Proof Assistant.
1 question
Use with coinductive types.
21 questions
when asking about proving theorems about or related to combinatorics, or when the question is related to combinatorics in some way,
2 questions
with commuting conversions or permutative conversions.
1 question
1
2 3 4 5
7