Corner cases

date:

Test

To compile:

alectryon --stdin-filename corner_cases.rst --frontend rst \
  -o corner_cases.html - < corner_cases.rst
    # Coq → HTML; produces ‘corner_cases.html’
alectryon corner_cases.rst -o corner_cases.xe.tex \
  --latex-dialect xelatex
    # Coq → LaTeX; produces ‘corner_cases.xe.tex’

Goal names

Goal True -> True /\ True.
True -> True /\ True
  intros; refine (conj ?[G1] ?[G2]).
H: True
G1
True
H: True
G2
True
  [G1]: exact I.
H: True
G2
True
  [G2]: exact I.
Qed.

Hypothesis bodies

Goal let a := (let bb := let b := 1 in (b , b)%nat in
              let tt := let t := nat in (t * t)%type in
              bb <: tt) in
     fst a = snd a.
let a :=
  let bb := let b := 1 in (b, b) in
  let tt := let t := nat in (t * t)%type in bb <: tt
  in
fst a = snd a
Proof.
let a :=
  let bb := let b := 1 in (b, b) in
  let tt := let t := nat in (t * t)%type in bb <: tt
  in
fst a = snd a
  intros.
a:= let bb := let b := 1 in (b, b) in
let tt := let t := nat in (t * t)%type in bb <: tt: let t := nat in t * t
fst a = snd a
  reflexivity.
Qed.

#a: - let bb := let b := 1 in (b, b) in let tt := let t := nat in (t * t)%type in bb <: tt - let t := nat in t * t

Self-reference

Definition a := 1.
Check corner_cases.a.
a
     : nat

Blanks at beginning of snippet

Goal True.
True

Trueexact I. Qed.

Blanks around sentences

Bubble:

Display all goals and responses

(* xyz *) Goal True /\ True.
True /\ True
  -
True /\ True idtac.
True /\ True
    pose (a := 1).
a:= 11: nat23
True /\ True
    (* xyz *) split.  (* xyz *)
a:= 1: nat
True
a:= 1: nat
True
    + (* xyz *)
a:= 1: nat
True idtac.
a:= 1: nat
True
      idtac.
a:= 1: nat
True (* x
      yz *)
      split.
    + (* xyz *)
a:= 1: nat
True { (* xyz *)
a:= 1: nat
True split. }
Qed. (* xyz *)

References

1, 2, 3, named_block.

Exercise directive

Exercise: Commutativity of addition

Goal forall x y: nat, x + y = y + x.
forall x y : nat, x + y = y + x
Abort.

Unicode in code

Definition test := "◆ ◉ ▲ ◧ ◎ ◴ ▶ ■".

Nesting and indentation

• Item

  Note

  Quote:

  • Item:

    Check nat.
    nat
         : Set

    • Rocq

      Check Prop.
      Prop
           : Type