-
+2
- 01
- 02
- 03
- 04
- 05
- 06
- 07
- 08
- 09
- 10
- 11
- 12
- 13
- 14
- 15
- 16
- 17
- 18
- 19
- 20
- 21
- 22
(* https://coq.inria.fr/library/Coq.Init.Datatypes.html *)
(* Basic boolean operators *)
Definition andb (b1 b2:bool) : bool := if b1 then b2 else false.
Definition orb (b1 b2:bool) : bool := if b1 then true else b2.
Definition implb (b1 b2:bool) : bool := if b1 then b2 else true.
Definition xorb (b1 b2:bool) : bool :=
match b1, b2 with
| true, true => false
| true, false => true
| false, true => true
| false, false => false
end.
Definition negb (b:bool) := if b then false else true.
Infix "||" := orb : bool_scope.
Infix "&&" := andb : bool_scope.
На первый взгляд этот ваш Coq (питух) выглядит как очередной ML-язычок.
j123123,
16 Сентября 2021
-
0
#85: https://govnokod.ru/27381 https://govnokod.xyz/_27381
#86: https://govnokod.ru/27405 https://govnokod.xyz/_27405
#87: https://govnokod.ru/27429 https://govnokod.xyz/_27429
#88: https://govnokod.ru/27432 https://govnokod.xyz/_27432
#89: https://govnokod.ru/27435 https://govnokod.xyz/_27435
#90: https://govnokod.ru/27439 https://govnokod.xyz/_27439
#91: https://govnokod.ru/27449 https://govnokod.xyz/_27449
#92: https://govnokod.ru/27460 https://govnokod.xyz/_27460
#93: https://govnokod.ru/27463 https://govnokod.xyz/_27463
#94: https://govnokod.ru/27466 https://govnokod.xyz/_27466
#95: https://govnokod.ru/27473 https://govnokod.xyz/_27473
#96: https://govnokod.ru/27478 https://govnokod.xyz/_27478
#97: https://govnokod.ru/27484 https://govnokod.xyz/_27484
#98: https://govnokod.ru/27495 https://govnokod.xyz/_27495
#99: https://govnokod.ru/27504 https://govnokod.xyz/_27504
#100: https://govnokod.ru/27508 https://govnokod.xyz/_27508
#101: https://govnokod.ru/27511 https://govnokod.xyz/_27511
#102: https://govnokod.ru/27518 https://govnokod.xyz/_27518
#103: https://govnokod.ru/27526 https://govnokod.xyz/_27526
#104: https://govnokod.ru/27534 https://govnokod.xyz/_27534
#105: https://govnokod.ru/27544 https://govnokod.xyz/_27544
#106: https://govnokod.ru/27552 https://govnokod.xyz/_27552
#107: https://govnokod.ru/27554 https://govnokod.xyz/_27554
#108: https://govnokod.ru/27557 https://govnokod.xyz/_27557
#109: https://govnokod.ru/27581 https://govnokod.xyz/_27581
#110: https://govnokod.ru/27610 https://govnokod.xyz/_27610
#111: https://govnokod.ru/27644 https://govnokod.xyz/_27644
#112: https://govnokod.ru/27648 https://govnokod.xyz/_27648
#113: https://govnokod.ru/27652 https://govnokod.xyz/_27652
#114: https://govnokod.ru/27659 https://govnokod.xyz/_27659
nepeKamHblu_nemyx,
14 Сентября 2021
-
+2
https://ideone.com/oO7f4I
3.14159265,
13 Сентября 2021
-
0
#84: https://govnokod.ru/27336 https://govnokod.xyz/_27336
#85: https://govnokod.ru/27381 https://govnokod.xyz/_27381
#86: https://govnokod.ru/27405 https://govnokod.xyz/_27405
#87: https://govnokod.ru/27429 https://govnokod.xyz/_27429
#88: https://govnokod.ru/27432 https://govnokod.xyz/_27432
#89: https://govnokod.ru/27435 https://govnokod.xyz/_27435
#90: https://govnokod.ru/27439 https://govnokod.xyz/_27439
#91: https://govnokod.ru/27449 https://govnokod.xyz/_27449
#92: https://govnokod.ru/27460 https://govnokod.xyz/_27460
#93: https://govnokod.ru/27463 https://govnokod.xyz/_27463
#94: https://govnokod.ru/27466 https://govnokod.xyz/_27466
#95: https://govnokod.ru/27473 https://govnokod.xyz/_27473
#96: https://govnokod.ru/27478 https://govnokod.xyz/_27478
#97: https://govnokod.ru/27484 https://govnokod.xyz/_27484
#98: https://govnokod.ru/27495 https://govnokod.xyz/_27495
#99: https://govnokod.ru/27504 https://govnokod.xyz/_27504
#100: https://govnokod.ru/27508 https://govnokod.xyz/_27508
#101: https://govnokod.ru/27511 https://govnokod.xyz/_27511
#102: https://govnokod.ru/27518 https://govnokod.xyz/_27518
#103: https://govnokod.ru/27526 https://govnokod.xyz/_27526
#104: https://govnokod.ru/27534 https://govnokod.xyz/_27534
#105: https://govnokod.ru/27544 https://govnokod.xyz/_27544
#106: https://govnokod.ru/27552 https://govnokod.xyz/_27552
#107: https://govnokod.ru/27554 https://govnokod.xyz/_27554
#108: https://govnokod.ru/27557 https://govnokod.xyz/_27557
#109: https://govnokod.ru/27581 https://govnokod.xyz/_27581
#110: https://govnokod.ru/27610 https://govnokod.xyz/_27610
#111: https://govnokod.ru/27644 https://govnokod.xyz/_27644
#112: https://govnokod.ru/27648 https://govnokod.xyz/_27648
#113: https://govnokod.ru/27652 https://govnokod.xyz/_27652
nepeKamHblu_nemyx,
11 Сентября 2021
-
+2
#83: https://govnokod.ru/27296 https://govnokod.xyz/_27296
#84: https://govnokod.ru/27336 https://govnokod.xyz/_27336
#85: https://govnokod.ru/27381 https://govnokod.xyz/_27381
#86: https://govnokod.ru/27405 https://govnokod.xyz/_27405
#87: https://govnokod.ru/27429 https://govnokod.xyz/_27429
#88: https://govnokod.ru/27432 https://govnokod.xyz/_27432
#89: https://govnokod.ru/27435 https://govnokod.xyz/_27435
#90: https://govnokod.ru/27439 https://govnokod.xyz/_27439
#91: https://govnokod.ru/27449 https://govnokod.xyz/_27449
#92: https://govnokod.ru/27460 https://govnokod.xyz/_27460
#93: https://govnokod.ru/27463 https://govnokod.xyz/_27463
#94: https://govnokod.ru/27466 https://govnokod.xyz/_27466
#95: https://govnokod.ru/27473 https://govnokod.xyz/_27473
#96: https://govnokod.ru/27478 https://govnokod.xyz/_27478
#97: https://govnokod.ru/27484 https://govnokod.xyz/_27484
#98: https://govnokod.ru/27495 https://govnokod.xyz/_27495
#99: https://govnokod.ru/27504 https://govnokod.xyz/_27504
#100: https://govnokod.ru/27508 https://govnokod.xyz/_27508
#101: https://govnokod.ru/27511 https://govnokod.xyz/_27511
#102: https://govnokod.ru/27518 https://govnokod.xyz/_27518
#103: https://govnokod.ru/27526 https://govnokod.xyz/_27526
#104: https://govnokod.ru/27534 https://govnokod.xyz/_27534
#105: https://govnokod.ru/27544 https://govnokod.xyz/_27544
#106: https://govnokod.ru/27552 https://govnokod.xyz/_27552
#107: https://govnokod.ru/27554 https://govnokod.xyz/_27554
#108: https://govnokod.ru/27557 https://govnokod.xyz/_27557
#109: https://govnokod.ru/27581 https://govnokod.xyz/_27581
#110: https://govnokod.ru/27610 https://govnokod.xyz/_27610
#111: https://govnokod.ru/27644 https://govnokod.xyz/_27644
#112: https://govnokod.ru/27648 https://govnokod.xyz/_27648
nepeKamHblu_nemyx,
08 Сентября 2021
-
−2
- 1
https://habr.com/ru/post/576818/
Мне очень не по себе при мысли о том, что до сих пор находятся на первый взгляд вполне адекватные и вменяемые люди моей и смежных профессий - программисты, админы и пр., - сознательно продолжающие работать на реализацию безумных идей все заблокировать, трафик проконтролировать и сломать интернет в попытках его "суверенизации".
Я не могу представить себе человека, доказавшего себе путем логических размышлений необходимость контроля трафика, реализовавшего и протестировавшего такой контроль, и при этом, не осознающего неминуемой опасности его применения для него самого, его родственников, друзей, знакомых и просто окружающих его людей.
Здесь не работают отмазки - я не знал, я выполнял ТЗ, я профессионал и пр. См. Нюрнбергские протоколы.
Поэтому я во-первых, призываю их подумать о том, что они попросту сами себе роют яму, создавая повышенные риски собственной успешной профессиональной и личной жизни.
Во-вторых, я повторю свое давнее обещание - если я замечу, что подобный человек, не раскаявшийся деятельно в своей деятельности, хочет устроиться в ту же компанию, где уже работаю (или работал) я, то я применю свое влияние в том объеме, который имею в этот момент, чтобы данный человек в эту компанию не попал.
В третьих - что я понимаю под деятельным раскаянием. Мне (и я надеюсь, нам - профессиональному сообществу) не нужны покаянные речи на публику, этим пусть занимаются те, кому речи являются профессией - политики или журналисты.
Деятельное раскаяние человека, причастного к IT, - это программа, сервис или библиотека функций под LGPL, выложенные на GitHub или подобном сервисе, предназначенные для нейтрализации того (или эквивалентного) вреда для беспрепятственного и свободного распространения информации, который он нанес, работая на безумцев.
JloJle4Ka,
08 Сентября 2021
-
0
#82: https://govnokod.ru/27284 https://govnokod.xyz/_27284
#83: https://govnokod.ru/27296 https://govnokod.xyz/_27296
#84: https://govnokod.ru/27336 https://govnokod.xyz/_27336
#85: https://govnokod.ru/27381 https://govnokod.xyz/_27381
#86: https://govnokod.ru/27405 https://govnokod.xyz/_27405
#87: https://govnokod.ru/27429 https://govnokod.xyz/_27429
#88: https://govnokod.ru/27432 https://govnokod.xyz/_27432
#89: https://govnokod.ru/27435 https://govnokod.xyz/_27435
#90: https://govnokod.ru/27439 https://govnokod.xyz/_27439
#91: https://govnokod.ru/27449 https://govnokod.xyz/_27449
#92: https://govnokod.ru/27460 https://govnokod.xyz/_27460
#93: https://govnokod.ru/27463 https://govnokod.xyz/_27463
#94: https://govnokod.ru/27466 https://govnokod.xyz/_27466
#95: https://govnokod.ru/27473 https://govnokod.xyz/_27473
#96: https://govnokod.ru/27478 https://govnokod.xyz/_27478
#97: https://govnokod.ru/27484 https://govnokod.xyz/_27484
#98: https://govnokod.ru/27495 https://govnokod.xyz/_27495
#99: https://govnokod.ru/27504 https://govnokod.xyz/_27504
#100: https://govnokod.ru/27508 https://govnokod.xyz/_27508
#101: https://govnokod.ru/27511 https://govnokod.xyz/_27511
#102: https://govnokod.ru/27518 https://govnokod.xyz/_27518
#103: https://govnokod.ru/27526 https://govnokod.xyz/_27526
#104: https://govnokod.ru/27534 https://govnokod.xyz/_27534
#105: https://govnokod.ru/27544 https://govnokod.xyz/_27544
#106: https://govnokod.ru/27552 https://govnokod.xyz/_27552
#107: https://govnokod.ru/27554 https://govnokod.xyz/_27554
#108: https://govnokod.ru/27557 https://govnokod.xyz/_27557
#109: https://govnokod.ru/27581 https://govnokod.xyz/_27581
#110: https://govnokod.ru/27610 https://govnokod.xyz/_27610
#111: https://govnokod.ru/27644 https://govnokod.xyz/_27644
nepeKamHblu_nemyx,
06 Сентября 2021
-
0
- 01
- 02
- 03
- 04
- 05
- 06
- 07
- 08
- 09
- 10
- 11
- 12
- 13
- 14
pub fn take(end: u32) -> u32
{
(0..).step_by(1000000000)
.map(|i| i * i)
.take_while(|&i| i < end)
.sum()
}
pub fn filter(end: u32) -> u32
{
(0..).step_by(1000000000)
.map(|i| i * i)
.filter(|&i| i < end)
.sum()
}
Решил вернуться к изучению багра rust.
Суть такова: код с take_while выводит 0, код с filter падает с runtime error или выбрасывается rustClang как бесконечный цикл (зависит от версии).
https://ideone.com/IS05Q0
То есть код filter ма-те-ма-ти-че-ски эквивалентен take_while. Поскольку i² монотонно возрастающая функция.
Из примера ниже можно убедиться что цикл на самом деле конечен.
https://ideone.com/xC2r35
Счётчик кидает ошибку при переполнении и range не зацикливается.
for x in (1..).step_by(1000000000) {
println!("{}", x);
}
1
1000000001
2000000001
Runtime error #stdin #stdout #stderr 0.01s 5552KB
3.14159265,
05 Сентября 2021
-
0
#81: https://govnokod.ru/27280 https://govnokod.xyz/_27280
#82: https://govnokod.ru/27284 https://govnokod.xyz/_27284
#83: https://govnokod.ru/27296 https://govnokod.xyz/_27296
#84: https://govnokod.ru/27336 https://govnokod.xyz/_27336
#85: https://govnokod.ru/27381 https://govnokod.xyz/_27381
#86: https://govnokod.ru/27405 https://govnokod.xyz/_27405
#87: https://govnokod.ru/27429 https://govnokod.xyz/_27429
#88: https://govnokod.ru/27432 https://govnokod.xyz/_27432
#89: https://govnokod.ru/27435 https://govnokod.xyz/_27435
#90: https://govnokod.ru/27439 https://govnokod.xyz/_27439
#91: https://govnokod.ru/27449 https://govnokod.xyz/_27449
#92: https://govnokod.ru/27460 https://govnokod.xyz/_27460
#93: https://govnokod.ru/27463 https://govnokod.xyz/_27463
#94: https://govnokod.ru/27466 https://govnokod.xyz/_27466
#95: https://govnokod.ru/27473 https://govnokod.xyz/_27473
#96: https://govnokod.ru/27478 https://govnokod.xyz/_27478
#97: https://govnokod.ru/27484 https://govnokod.xyz/_27484
#98: https://govnokod.ru/27495 https://govnokod.xyz/_27495
#99: https://govnokod.ru/27504 https://govnokod.xyz/_27504
#100: https://govnokod.ru/27508 https://govnokod.xyz/_27508
#101: https://govnokod.ru/27511 https://govnokod.xyz/_27511
#102: https://govnokod.ru/27518 https://govnokod.xyz/_27518
#103: https://govnokod.ru/27526 https://govnokod.xyz/_27526
#104: https://govnokod.ru/27534 https://govnokod.xyz/_27534
#105: https://govnokod.ru/27544 https://govnokod.xyz/_27544
#106: https://govnokod.ru/27552 https://govnokod.xyz/_27552
#107: https://govnokod.ru/27554 https://govnokod.xyz/_27554
#108: https://govnokod.ru/27557 https://govnokod.xyz/_27557
#109: https://govnokod.ru/27581 https://govnokod.xyz/_27581
#110: https://govnokod.ru/27610 https://govnokod.xyz/_27610
nepeKamHblu_nemyx,
03 Сентября 2021
-
+1
- 01
- 02
- 03
- 04
- 05
- 06
- 07
- 08
- 09
- 10
- 11
- 12
public class RegLocalityPK
implements Serializable
{
private String countryNo;
private String govNo;
private String localityNo;
public String getGovNo()
{
return this.govNo;
}
…
IIIyqpymuHckuu_nemyx,
03 Сентября 2021