Questions tagged [definition]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
2 votes
1 answer

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. ...
Molossus Spondee's user avatar
1 vote
1 answer

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 ...
Pieter Cuijpers's user avatar
5 votes
2 answers

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 ...
Pieter Cuijpers's user avatar
0 votes
1 answer

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,...
with-forest's user avatar
5 votes
0 answers

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 ...
user695931's user avatar
3 votes
2 answers

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-...
Greg Nisbet's user avatar
  • 2,671