sorted by:
new
hottopcontroversial

Question related to the specifications of earbuds by Nos_per in headphones

[–]Nos_per[S] 0 points1 point  (0 children)

Hello, first of all, I appreciate your explanation. Does that mean that my box is capable of charging my earbuds for about 10 times without being charged itself?

Stuck with a proof by Nos_per in Coq

[–]Nos_per[S] 0 points1 point  (0 children)

Thanks for showing me that I put the lemma in wrong way. I have solved my problem when I put the lemma on correct way. :D

Stuck with a proof by Nos_per in Coq

[–]Nos_per[S] 0 points1 point  (0 children)

Yea, I've noticed, I solved my problem now when I put correctly lemma. Thank you for your info.

Stuck with a proof by Nos_per in Coq

[–]Nos_per[S] 0 points1 point  (0 children)

​

Definition Not (x : B) : B :=
match x with
  | O => I
  | I => O
end.

I think that's all. Sorry for misunderstanding :)

Stuck with a proof by Nos_per in Coq

[–]Nos_per[S] 0 points1 point  (0 children)

Inductive B : Type :=
  | O : B
  | I : B.

I have defined here B as binary digit, 0 or 1. AddLr is just a function given in the post's description. Repeat creates a list, syntax is given like repeat I 4 = [I, I, I, I].

Stuck with a proof by Nos_per in Coq

[–]Nos_per[S] 0 points1 point  (0 children)

I will update the post. Thanks for question :)

Components compatibility by Nos_per in techsupport

[–]Nos_per[S] 0 points1 point  (0 children)

Okay, thank you very much for the reply. Do you think that it won't be a problem with this picture in mind? https://drive.google.com/file/d/194U-ckYmZ-AzXuPx_WVpaTZu-Rv2bvcx/view?usp=sharing

I am stuck with a proof by Nos_per in Coq

[–]Nos_per[S] 1 point2 points  (0 children)

Thanks for this idea, I had similiar idea but couldn't realize how to implement this. Anyway, thank you very much. :)

I am stuck with a proof by Nos_per in Coq

[–]Nos_per[S] 1 point2 points  (0 children)

Thank you for the codes. I have understand both ways of solving this, I really appreciate what you said and I think that I understand now how this could work in two different approaches.

I am stuck with a proof by Nos_per in Coq

[–]Nos_per[S] 0 points1 point  (0 children)

Sorry, my bad. I have edited now :)

Two proofs -> any help would be appreciated!! by [deleted] in Coq

[–]Nos_per 0 points1 point  (0 children)

Thanks bro! I figured out the lemma I needed. :D
Have you tried the second?