User Charlie Parker

6 votes

0 answers

196 views

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

asked Jul 9, 2022 at 19:39

6 votes

0 answers

87 views

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

asked Jul 14, 2022 at 19:19

3 votes

1 answer

292 views

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

asked Feb 23 at 20:26

2 votes

1 answer

95 views

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

asked Feb 29 at 1:40

2 votes

1 answer

119 views

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

asked Mar 2 at 2:37

2 votes

1 answer

549 views

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

asked Apr 9 at 19:47

1 vote

2 answers

145 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?

asked May 27 at 23:58

1 vote

1 answer

260 views

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

asked Mar 5 at 20:31

1 vote

1 answer

249 views

Where does one find the keyword documentation for Lean4?

asked Feb 29 at 1:25

1 vote

0 answers

26 views

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

asked Jul 15, 2022 at 23:16

1 vote

1 answer

343 views

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

asked Nov 11, 2022 at 5:30

1 vote

2 answers

290 views

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

asked Feb 22 at 20:49

0 votes

0 answers

33 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?

asked Feb 22 at 21:03

0 votes

1 answer

123 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?

asked Mar 4 at 20:34

0 votes

3 answers

239 views

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

asked Feb 29 at 1:04

0 votes

1 answer

85 views

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

asked Mar 15 at 4:48

0 votes

0 answers

38 views

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

asked Jun 3 at 23:59

Stack Exchange Network

17 Questions

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

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

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

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

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

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

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?

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

Where does one find the keyword documentation for Lean4?

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

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

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

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?

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

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

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

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