Not visible text in the dark format

[janidziakhb]

Description

Not visible text in the dark format

(Optional:) Please add any files, screenshots, or other information here.

No response

(Required) What is this issue most closely related to? Select one.

Choose One

Internal issue ID

6186ff17-9288-4755-9edf-78e0b8ca7b69

Paper URL

https://arxiv.org/html/2405.04282v1

Browser

Chrome/124.0.0.0

Device Type

Desktop

[html-feedback-bot[bot]]

Location in document: ltx_caption

Selected HTML:

1Require Import List.

2Lemma rev_append: forall {a} (l1 l2: list a),

3 rev (l1 ++ l2) = rev l2 ++ rev l1.

4Proof.

5intros a l1 l2. induction l1; intros.

6 - simpl. rewrite app_nil_r. reflexivity.

7 - simpl. rewrite IHl1.

8Admitted.

Listing 1: Example Coq file test.v with a property of rev.

Report issue for preceding element

⬇

1with ProofFile("test.v") as pf:

2 pf.exec(len(pf.steps))

3 print(pf.context)

4 for proof in pf.proofs:

5 for step in proof.steps:

6 print(step.text, step.ast, step.context, step.goals)

Listing 2: Proof data a

[github-actions[bot]]

Hello @janidziakhb, thanks for the issue report! We are reviewing your report and will address it as soon as possible.