Skip to content

Commit

Permalink
r4166
Browse files Browse the repository at this point in the history
  • Loading branch information
@liyishuai
liyishuai committed Apr 23, 2024
1 parent 5bd384b commit 50290bd
Show file tree
Hide file tree
Showing 354 changed files with 44,109 additions and 40,190 deletions.
2 changes: 1 addition & 1 deletion lf-current/AltAuto.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2410,7 +2410,7 @@ <h1 class="libtitle">AltAuto<span class="subtitle">A Streamlined Treatment of Au
</div>
<div class="code">

<span class="comment">(*&nbsp;2023-12-24&nbsp;12:53&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;2024-04-23&nbsp;03:46&nbsp;*)</span><br/>
</div>
</div>

Expand Down
2 changes: 1 addition & 1 deletion lf-current/AltAuto.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1825,4 +1825,4 @@ Definition manual_grade_for_nor_intuition : option (nat*string) := None.
- Ltac functions and [match goal] *)

(* 2023-12-24 12:53 *)
(* 2024-04-23 03:46 *)
2 changes: 1 addition & 1 deletion lf-current/AltAutoTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -255,4 +255,4 @@ idtac "---------- nor_intuition ---------".
idtac "MANUAL".
Abort.

(* 2023-12-24 12:53 *)
(* 2024-04-23 03:46 *)
2 changes: 1 addition & 1 deletion lf-current/Auto.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -910,7 +910,7 @@ <h1 class="libtitle">Auto<span class="subtitle">More Automation</span></h1>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">P</span> <span class="id" title="var">Q</span> <span class="id" title="var">HP</span> <span class="id" title="var">HQ</span>. <span class="id" title="tactic">destruct</span> <span class="id" title="var">HP</span> <span class="id" title="keyword">as</span> [<span class="id" title="var">y</span> <span class="id" title="var">HP'</span>]. <span class="id" title="tactic">eauto</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;2023-12-24&nbsp;12:53&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;2024-04-23&nbsp;03:46&nbsp;*)</span><br/>
</div>
</div>

Expand Down
2 changes: 1 addition & 1 deletion lf-current/Auto.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -740,4 +740,4 @@ Proof.
intros P Q HP HQ. destruct HP as [y HP']. eauto.
Qed.

(* 2023-12-24 12:53 *)
(* 2024-04-23 03:46 *)
2 changes: 1 addition & 1 deletion lf-current/AutoTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -63,4 +63,4 @@ idtac "".
idtac "********** Advanced **********".
Abort.

(* 2023-12-24 12:53 *)
(* 2024-04-23 03:46 *)
2 changes: 1 addition & 1 deletion lf-current/Basics.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2691,7 +2691,7 @@ <h1 class="libtitle">Basics<span class="subtitle">Functional Programming in Coq<
</div>
<div class="code">

<span class="comment">(*&nbsp;2023-12-24&nbsp;12:53&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;2024-04-23&nbsp;03:45&nbsp;*)</span><br/>
</div>
</div>

Expand Down
2 changes: 1 addition & 1 deletion lf-current/Basics.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2015,4 +2015,4 @@ Example test_bin_incr6 :
output. But since they have to be graded by a human, the test
script won't be able to tell you much about them. *)

(* 2023-12-24 12:53 *)
(* 2024-04-23 03:45 *)
2 changes: 1 addition & 1 deletion lf-current/BasicsTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -521,4 +521,4 @@ idtac "".
idtac "********** Advanced **********".
Abort.

(* 2023-12-24 12:53 *)
(* 2024-04-23 03:46 *)
2 changes: 1 addition & 1 deletion lf-current/Bib.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -84,7 +84,7 @@ <h1 class="libtitle">Bib<span class="subtitle">Bibliography</span></h1>
</div>
<div class="code">

<span class="comment">(*&nbsp;2023-12-24&nbsp;12:53&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;2024-04-23&nbsp;03:46&nbsp;*)</span><br/>
</div>
</div>

Expand Down
2 changes: 1 addition & 1 deletion lf-current/Bib.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,4 +32,4 @@
*)

(* 2023-12-24 12:53 *)
(* 2024-04-23 03:46 *)
2 changes: 1 addition & 1 deletion lf-current/BibTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -63,4 +63,4 @@ idtac "".
idtac "********** Advanced **********".
Abort.

(* 2023-12-24 12:53 *)
(* 2024-04-23 03:46 *)
2 changes: 1 addition & 1 deletion lf-current/Extraction.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -232,7 +232,7 @@ <h1 class="libtitle">Extraction<span class="subtitle">Extracting OCaml from Coq<
</div>
<div class="code">

<span class="comment">(*&nbsp;2023-12-24&nbsp;12:53&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;2024-04-23&nbsp;03:46&nbsp;*)</span><br/>
</div>
</div>

Expand Down
2 changes: 1 addition & 1 deletion lf-current/Extraction.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -129,4 +129,4 @@ Extraction "imp.ml" empty_st ceval_step parse.
chapter in _Verified Functional Algorithms_ (_Software
Foundations_ volume 3). *)

(* 2023-12-24 12:53 *)
(* 2024-04-23 03:46 *)
2 changes: 1 addition & 1 deletion lf-current/ExtractionTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -63,4 +63,4 @@ idtac "".
idtac "********** Advanced **********".
Abort.

(* 2023-12-24 12:53 *)
(* 2024-04-23 03:46 *)
82 changes: 80 additions & 2 deletions lf-current/Imp.html
View file

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion lf-current/Imp.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2077,4 +2077,4 @@ End BreakImp.
[] *)

(* 2023-12-24 12:53 *)
(* 2024-04-23 03:46 *)
2 changes: 1 addition & 1 deletion lf-current/ImpCEvalFun.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -481,7 +481,7 @@ <h1 class="libtitle">ImpCEvalFun<span class="subtitle">An Evaluation Function fo
</div>

<br/>
<span class="comment">(*&nbsp;2023-12-24&nbsp;12:53&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;2024-04-23&nbsp;03:46&nbsp;*)</span><br/>
</div>
</div>

Expand Down
4 changes: 2 additions & 2 deletions lf-current/ImpCEvalFun.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -214,7 +214,7 @@ Example pup_to_n_1 :
test_ceval (X !-> 5) pup_to_n
= Some (0, 15, 0).
(* FILL IN HERE *) Admitted.
(*
(*
Proof. reflexivity. Qed.
*)
(** [] *)
Expand Down Expand Up @@ -393,4 +393,4 @@ Proof.
rewrite E1 in E2. inversion E2. reflexivity.
lia. lia. Qed.

(* 2023-12-24 12:53 *)
(* 2024-04-23 03:46 *)
2 changes: 1 addition & 1 deletion lf-current/ImpCEvalFunTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -91,4 +91,4 @@ idtac "---------- ceval_step__ceval_inf ---------".
idtac "MANUAL".
Abort.

(* 2023-12-24 12:53 *)
(* 2024-04-23 03:46 *)
2 changes: 1 addition & 1 deletion lf-current/ImpParser.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -536,7 +536,7 @@ <h1 class="libtitle">ImpParser<span class="subtitle">Lexing and Parsing in Coq</
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Imp.html#:com:com_scope:'while'_x_'do'_x_'end'"><span class="id" title="notation">end</span></a><a class="idref" href="Imp.html#313afe74ec81f2da17d8e7bca3b042e<sub>7</sub>"><span class="id" title="notation">;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"x" <a class="idref" href="Imp.html#91e9aa710642047a93142bdf557f1a1b"><span class="id" title="notation">:=</span></a> "z" <a class="idref" href="Imp.html#23430cd9e427d30c054d4f029e39cb7f"><span class="id" title="notation">}&gt;</span></a>.<br/>
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">cbv</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;2023-12-24&nbsp;12:53&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;2024-04-23&nbsp;03:46&nbsp;*)</span><br/>
</div>
</div>

Expand Down
2 changes: 1 addition & 1 deletion lf-current/ImpParser.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -462,4 +462,4 @@ Example eg2 : parse "
"x" := "z" }>.
Proof. cbv. reflexivity. Qed.

(* 2023-12-24 12:53 *)
(* 2024-04-23 03:46 *)
2 changes: 1 addition & 1 deletion lf-current/ImpParserTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -63,4 +63,4 @@ idtac "".
idtac "********** Advanced **********".
Abort.

(* 2023-12-24 12:53 *)
(* 2024-04-23 03:46 *)
2 changes: 1 addition & 1 deletion lf-current/ImpTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -314,4 +314,4 @@ idtac "---------- BreakImp.seq_stops_on_break ---------".
Print Assumptions BreakImp.seq_stops_on_break.
Abort.

(* 2023-12-24 12:53 *)
(* 2024-04-23 03:46 *)
2 changes: 1 addition & 1 deletion lf-current/IndPrinciples.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1361,7 +1361,7 @@ <h1 class="libtitle">IndPrinciples<span class="subtitle">Induction Principles</s

<div class="code">

<span class="comment">(*&nbsp;2023-12-24&nbsp;12:53&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;2024-04-23&nbsp;03:46&nbsp;*)</span><br/>
</div>
</div>

Expand Down
6 changes: 3 additions & 3 deletions lf-current/IndPrinciples.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -302,7 +302,7 @@ Check tree_ind.
(forall m : mytype X, P m ->
forall n : nat, P (constr3 X m n)) ->
forall m : mytype X, P m
*)
*)
(** [] *)

(** **** Exercise: 1 star, standard, optional (foo)
Expand All @@ -317,7 +317,7 @@ Check tree_ind.
(forall f1 : nat -> foo X Y,
(forall n : nat, P (f1 n)) -> P (quux X Y f1)) ->
forall f2 : foo X Y, P f2
*)
*)
(** [] *)

(** **** Exercise: 1 star, standard, optional (foo')
Expand Down Expand Up @@ -963,4 +963,4 @@ Proof. (* FILL IN HERE *) Admitted.

(** [] *)

(* 2023-12-24 12:53 *)
(* 2024-04-23 03:46 *)
2 changes: 1 addition & 1 deletion lf-current/IndPrinciplesTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -109,4 +109,4 @@ idtac "".
idtac "********** Advanced **********".
Abort.

(* 2023-12-24 12:53 *)
(* 2024-04-23 03:46 *)
4 changes: 2 additions & 2 deletions lf-current/IndProp.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -109,7 +109,7 @@ <h1 class="libtitle">IndProp<span class="subtitle">Inductively Defined Propositi
<div class="code">

<span class="id" title="var">Fail</span> <span class="id" title="keyword">Fixpoint</span> <a id="reaches_1_in" class="idref" href="#reaches_1_in"><span class="id" title="definition">reaches_1_in</span></a> (<a id="n:5" class="idref" href="#n:5"><span class="id" title="binder">n</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">if</span> <a class="idref" href="IndProp.html#n:5"><span class="id" title="variable">n</span></a> <a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">=?</span></a> 1 <span class="id" title="keyword">then</span> <a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a><br/>
&nbsp;&nbsp;<span class="id" title="keyword">if</span> <a class="idref" href="IndProp.html#n:5"><span class="id" title="variable">n</span></a> <a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">=?</span></a> 1 <span class="id" title="keyword">then</span> 0<br/>
&nbsp;&nbsp;<span class="id" title="keyword">else</span> 1 <a class="idref" href="Basics.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <a class="idref" href="IndProp.html#reaches_1_in:6"><span class="id" title="definition">reaches_1_in</span></a> (<a class="idref" href="IndProp.html#f"><span class="id" title="definition">f</span></a> <a class="idref" href="IndProp.html#n:5"><span class="id" title="variable">n</span></a>).<br/>
</div>

Expand Down Expand Up @@ -3320,7 +3320,7 @@ <h1 class="libtitle">IndProp<span class="subtitle">Inductively Defined Propositi

<div class="code">

<span class="comment">(*&nbsp;2023-12-24&nbsp;12:53&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;2024-04-23&nbsp;03:45&nbsp;*)</span><br/>
</div>
</div>

Expand Down
12 changes: 6 additions & 6 deletions lf-current/IndProp.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,7 @@ Definition f (n : nat) :=
that it takes for such a sequence to reach [1]. *)

Fail Fixpoint reaches_1_in (n : nat) :=
if n =? 1 then true
if n =? 1 then 0
else 1 + reaches_1_in (f n).

(** This definition is rejected by Coq's termination checker, since
Expand Down Expand Up @@ -1862,27 +1862,27 @@ Inductive nostutter {X:Type} : list X -> Prop :=

Example test_nostutter_1: nostutter [3;1;4;1;5;6].
(* FILL IN HERE *) Admitted.
(*
(*
Proof. repeat constructor; apply eqb_neq; auto.
Qed.
*)

Example test_nostutter_2: nostutter (@nil nat).
(* FILL IN HERE *) Admitted.
(*
(*
Proof. repeat constructor; apply eqb_neq; auto.
Qed.
*)

Example test_nostutter_3: nostutter [5].
(* FILL IN HERE *) Admitted.
(*
(*
Proof. repeat constructor; auto. Qed.
*)

Example test_nostutter_4: not (nostutter [3;1;1;4]).
(* FILL IN HERE *) Admitted.
(*
(*
Proof. intro.
repeat match goal with
h: nostutter _ |- _ => inversion h; clear h; subst
Expand Down Expand Up @@ -2433,4 +2433,4 @@ Proof.
(* FILL IN HERE *) Admitted.
(** [] *)

(* 2023-12-24 12:53 *)
(* 2024-04-23 03:45 *)
2 changes: 1 addition & 1 deletion lf-current/IndPropTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -332,4 +332,4 @@ idtac "---------- merge_filter ---------".
Print Assumptions merge_filter.
Abort.

(* 2023-12-24 12:53 *)
(* 2024-04-23 03:46 *)
2 changes: 1 addition & 1 deletion lf-current/Induction.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1055,7 +1055,7 @@ <h1 class="libtitle">Induction<span class="subtitle">Proof by Induction</span></

<div class="code">

<span class="comment">(*&nbsp;2023-12-24&nbsp;12:53&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;2024-04-23&nbsp;03:45&nbsp;*)</span><br/>
</div>
</div>

Expand Down
2 changes: 1 addition & 1 deletion lf-current/Induction.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -761,4 +761,4 @@ Proof.

(** [] *)

(* 2023-12-24 12:53 *)
(* 2024-04-23 03:45 *)
2 changes: 1 addition & 1 deletion lf-current/InductionTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -258,4 +258,4 @@ idtac "---------- bin_nat_bin ---------".
Print Assumptions bin_nat_bin.
Abort.

(* 2023-12-24 12:53 *)
(* 2024-04-23 03:46 *)
2 changes: 1 addition & 1 deletion lf-current/LICENSE
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
Copyright (c) 2023
Copyright (c) 2024

Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
Expand Down
2 changes: 1 addition & 1 deletion lf-current/Lists.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1522,7 +1522,7 @@ <h1 class="libtitle">Lists<span class="subtitle">Working with Structured Data</s

<div class="code">
<span class="id" title="keyword">End</span> <a class="idref" href="Lists.html#PartialMap"><span class="id" title="module">PartialMap</span></a>.<br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;2023-12-24&nbsp;12:53&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;2024-04-23&nbsp;03:45&nbsp;*)</span><br/>
</div>
</div>

Expand Down
2 changes: 1 addition & 1 deletion lf-current/Lists.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1137,4 +1137,4 @@ Proof.
(** [] *)
End PartialMap.

(* 2023-12-24 12:53 *)
(* 2024-04-23 03:45 *)
2 changes: 1 addition & 1 deletion lf-current/ListsTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -516,4 +516,4 @@ idtac "---------- NatList.rev_injective ---------".
Print Assumptions NatList.rev_injective.
Abort.

(* 2023-12-24 12:53 *)
(* 2024-04-23 03:46 *)
2 changes: 1 addition & 1 deletion lf-current/Logic.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2402,7 +2402,7 @@ <h1 class="libtitle">Logic<span class="subtitle">Logic in Coq</span></h1>

<div class="code">

<span class="comment">(*&nbsp;2023-12-24&nbsp;12:53&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;2024-04-23&nbsp;03:45&nbsp;*)</span><br/>
</div>
</div>

Expand Down
2 changes: 1 addition & 1 deletion lf-current/Logic.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1734,4 +1734,4 @@ Definition implies_to_or := forall P Q:Prop,

[] *)

(* 2023-12-24 12:53 *)
(* 2024-04-23 03:45 *)
2 changes: 1 addition & 1 deletion lf-current/LogicTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -414,4 +414,4 @@ idtac "---------- not_exists_dist ---------".
Print Assumptions not_exists_dist.
Abort.

(* 2023-12-24 12:53 *)
(* 2024-04-23 03:46 *)
2 changes: 1 addition & 1 deletion lf-current/Maps.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -562,7 +562,7 @@ <h1 class="libtitle">Maps<span class="subtitle">Total and Partial Maps</span></h
</div>
<div class="code">

<span class="comment">(*&nbsp;2023-12-24&nbsp;12:53&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;2024-04-23&nbsp;03:45&nbsp;*)</span><br/>
</div>
</div>

Expand Down
2 changes: 1 addition & 1 deletion lf-current/Maps.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -379,4 +379,4 @@ Qed.
used to keep track of which program variables are defined in a
given scope. *)

(* 2023-12-24 12:53 *)
(* 2024-04-23 03:45 *)
2 changes: 1 addition & 1 deletion lf-current/MapsTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -94,4 +94,4 @@ idtac "".
idtac "********** Advanced **********".
Abort.

(* 2023-12-24 12:53 *)
(* 2024-04-23 03:46 *)
2 changes: 1 addition & 1 deletion lf-current/Poly.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1735,7 +1735,7 @@ <h1 class="libtitle">Poly<span class="subtitle">Polymorphism and Higher-Order Fu

<span class="id" title="keyword">End</span> <a class="idref" href="Poly.html#Exercises.Church"><span class="id" title="module">Church</span></a>.<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="Poly.html#Exercises"><span class="id" title="module">Exercises</span></a>.<br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;2023-12-24&nbsp;12:53&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;2024-04-23&nbsp;03:45&nbsp;*)</span><br/>
</div>
</div>

Expand Down
2 changes: 1 addition & 1 deletion lf-current/Poly.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1224,4 +1224,4 @@ Proof. (* FILL IN HERE *) Admitted.
End Church.
End Exercises.

(* 2023-12-24 12:53 *)
(* 2024-04-23 03:45 *)
2 changes: 1 addition & 1 deletion lf-current/PolyTest.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -498,4 +498,4 @@ idtac "---------- Exercises.Church.exp_3 ---------".
Print Assumptions Exercises.Church.exp_3.
Abort.

(* 2023-12-24 12:53 *)
(* 2024-04-23 03:46 *)
2 changes: 1 addition & 1 deletion lf-current/Postscript.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -217,7 +217,7 @@ <h1 class="libtitle">Postscript</h1>
</div>
<div class="code">

<span class="comment">(*&nbsp;2023-12-24&nbsp;12:53&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;2024-04-23&nbsp;03:46&nbsp;*)</span><br/>
</div>
</div>

Expand Down
Loading

0 comments on commit 50290bd

Please sign in to comment.