Skip to main content
Charlie Parker's user avatar
Charlie Parker's user avatar
Charlie Parker's user avatar
Charlie Parker
  • Member for 2 years, 2 months
  • Last seen more than a week ago
0 votes
0 answers
18 views

How does one install new dependencies to a Lean 4 programatically e.g., adding aesop by editing lakefile.lean in bash?

1 vote
2 answers
87 views

How to write a proof of n + 0 = n in Lean 4 using the built in definition of addition for Nats and not the theorem for Nat.add_zero?

2 votes
1 answer
399 views

How does one import Natural numbers in Lean 4 -- unknown identifier 'ℕ'?

0 votes
1 answer
68 views

How does one define a structure with the ext theorem in Lean 4?

1 vote
1 answer
133 views

How do I force Lean 4 to show me the rewrite rules and theorems simp is using -- error: unknown option 'trace.simplify.rewrite'?

0 votes
1 answer
91 views

Given some proposition in Lean 4, how do we state a theorem saying that we want that property to hold a number of times?

2 votes
1 answer
94 views

How do I explicitly see the propositional or logical constructors in Lean 4?

2 votes
1 answer
61 views

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

1 vote
1 answer
137 views

Where does one find the keyword documentation for Lean4?

0 votes
3 answers
128 views

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

3 votes
1 answer
156 views

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

0 votes
0 answers
24 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?

1 vote
2 answers
154 views

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

1 vote
1 answer
268 views

How does one translate Lean to Coq (and visa versa)?

1 vote
0 answers
26 views

Why does TacArg accepts a value of CAst.t type when it should only accept values of types?

6 votes
0 answers
80 views

What are Generic Arguments in Coq and how are they structured in their OCaml code?

6 votes
0 answers
188 views

How does one systematically traverse OCaml representations of Coq ASTs terms?