Explore our questions

0 votes
2 answers
18 views

Why can't Lean4 evaluate my function despite it being defined, Error: compiler IR check failed at '_eval', error: unknown declaration 'g'?

1 vote
1 answer
22 views

Where does one find the keyword documentation for Lean4?

1 vote
1 answer
50 views

Binding variables to terms involving later variables

2 votes
2 answers
111 views

How exactly solved metas "revisited" in an efficient dependent type checker?

0 votes
1 answer
11 views

How do I construct a concrete real number in lean without errors? failed to synthesize instance OfScientific ℝ

1 vote
2 answers
79 views

How does one create a lean project and have mathlib import work when not creating the lean project at the $HOME directory?

6 votes
1 answer
178 views

What are the principal differences between Agda's core type theory and Coq's?

1 vote
1 answer
36 views

Using coIH as an argument to the transitivity of Bisimilarity (cofix and pcofix)

1 vote
1 answer
34 views

How do I write bitwise logic in lean4 with mathlib?

2 votes
1 answer
149 views

What is the well-established η law for naturals?

2 votes
1 answer
52 views

What is the official way to reinstall Lean4 from scratch on a Mac or Linux?

2 votes
3 answers
94 views

Induction on indexed type family without JMeq

0 votes
1 answer
46 views

Coq - Overloading over multiple parameters with canonical structures

0 votes
0 answers
18 views

How does one create a lean project even if it already exists e.g., lake +leanprover/lean4:nightly-2023-02-04 new my_project math?

Browse more Questions