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, 1 month
  • Last seen more than a week ago
6 votes
0 answers
185 views

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

6 votes
0 answers
80 views

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

2 votes
1 answer
120 views

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

2 votes
1 answer
60 views

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

2 votes
1 answer
90 views

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

2 votes
1 answer
371 views

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

1 vote
1 answer
101 views

Where does one find the keyword documentation for Lean4?

1 vote
1 answer
105 views

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

1 vote
0 answers
26 views

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

1 vote
1 answer
255 views

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

1 vote
2 answers
127 views

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

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

0 votes
1 answer
80 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?

0 votes
3 answers
101 views

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

0 votes
1 answer
64 views

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