Skip to main content
Stack Overflow
  1. About
  3. For Teams
Filter by
Sorted by
Tagged with
0 votes
1 answer
56 views

When I am testing the examples in Theorem Proving in Lean4 , I find out that command #check Implies threw an error : unknown identifier Implies. I tried #print And and find out that it is a struct : ...
0 votes
1 answer
114 views

Background As the Lean Reference's Instances for nested types example shows, in a function that implements a type class method for a certain type, one can already use the type class instance for that ...
1 vote
1 answer
118 views

I just started to learn lean and I am confused about theorem and lemma. If I understood correctly, these keywords are interchangeable and it is just a matter of theorem being a more important result ...
roi_saumon's user avatar
1 vote
1 answer
95 views

abbrev Vec (α : Type) (n : Nat) := Fin n → α def Vec.map2 {α β φ n} (f : α → β → φ) (v1 : Vec α n) (v2 : Vec β n) : Vec φ n := fun i ↦ f (v1 i) (v2 i) def Vec.add {α n} [Add α] (v1 v2 : Vec α n) : ...
1 vote
1 answer
83 views

I'm trying to work through Purely Functional Data Structures in Lean 4, and the first exercise is to create a function suffixes that returns a list of lists, where each list is a suffix. Here's my ...
0 votes
0 answers
76 views

I am trying to install Lean CLI on Windows 10 inside a virtual environment (venv), but after installation I do not see the backtest command. Here are the exact steps I did: Created and activated a ...
0 votes
1 answer
84 views

I have the following 2 definitions of length function: def primesUnder10 : List Nat := [2, 3, 5, 7] def length1 (α : Type) (xs : List α) : Nat := match xs with | [] => Nat.zero | y::ys => ...
R71's user avatar
  • 4,573
0 votes
1 answer
53 views

example (i:Fin 9)(h:(i.1/3 :Fin 3).1 = i/3): 0 = i.1/3:= by simp at h exact h This finishes the proof, but if i = 6, then h certainly is true. But the claim is 0 = i.1/3 <=> 0 = 2 either ...
0 votes
0 answers
96 views

In Haskell I can hide the Prelude by writing import Prelude () or I can hide specific symbols by writing (e.g.) import Prelude hiding (Bool) How do I do the same thing in Lean? When I tried open ...
eyelash's user avatar
  • 4,146
2 votes
1 answer
141 views

I am learning lean4 both as a functional programming language and a theorem prover. One of the very useful data structure in programming is an iterator (or an infinite list) that seems to not builtin ...
khanh's user avatar
  • 684
1 vote
1 answer
111 views

Let's say I want to write a function that takes an argument of any type and returns true if and only if the type of the argument is String. How would I do that? The following code def isString {T : ...
eyelash's user avatar
  • 4,146
0 votes
0 answers
65 views

I'm attempting to solve the DMOJ problem Tree Tasks(https://dmoj.ca/problem/treepractice1), which involves computing the diameter and radius of a weighted tree. My goal is to implement a solution in ...
0 votes
1 answer
226 views

I just started using lean. I was trying to compile a simple hello world program without using lake at first (I will checkout lake also). In my working directory I have 2 files. The first one is: -- ...
roi_saumon's user avatar
2 votes
1 answer
196 views

I am quite comfortable with Agda. I decided to experiment with Lean, but I find that propositional equality is really messing with me. Sometimes I find that rfl just works, but at other times it doesn'...
1 vote
1 answer
71 views

I would like to define a DSL for writing lambda terms in Lean using macros a la the arithmetic example. I want to support syntax for multiple arguments in the lambda, and left-associativity. Thus far, ...

15 30 50 per page
1
2 3 4 5
...
16

AltStyle によって変換されたページ (->オリジナル) /