Charlie Parker's user avatar
Charlie Parker's user avatar
Charlie Parker's user avatar
Charlie Parker
  • Member for 2 years
  • Last seen this week
6 votes
0 answers
184 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
85 views

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

2 votes
1 answer
53 views

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

2 votes
1 answer
81 views

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

2 votes
1 answer
333 views

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

1 vote
1 answer
75 views

Where does one find the keyword documentation for Lean4?

1 vote
1 answer
52 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
227 views

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

1 vote
2 answers
106 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
21 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
73 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
69 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
59 views

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