Questions tagged [definition]
The definition tag has no usage guidance.
How do clausal definitions work?
I'm most familiar with the metatheory of calculi based around expressions. But systems like Agda use separate clauses for definitions. ...
Question about default definitions in fields
In Unclarity about Preorder class in Lean4 I asked why the third and fourth field (lt and lt_iff_le_not_le) in the definition of MyPreorder below would both be necessary, as one follows from the other ...
Unclarity about Preorder class in Lean4
I realize the port of Mathlib to Lean4 is not finished yet, but I've run into a definition that I do not quite understand. I'm quite new at using theoremprovers as well as stackexchange, so please be ...
Define a function using another function
I want to define a translation function g from another function f. Definition trans (f g : Q -> Q) (t : Q) := forall q : Q, f (q + t) == g q. In the above code,...
An algorithm for the substitution of formulas for predicates in first order logic
I am trying to find a detailed description of the definition of substitution of formulas for predicates in first order logic and an implementation of this as a function in Lean or Haskell. The aim is ...
Coq defining a hierarchy of collections of integers with infinitely many "levels"
I'm trying to formalize a small part of higher-order arithmetic in Coq as an exercise (Wikipedia article for second-order arithmetic). It's straightforward to formalize something resembling second-...