Commit 1d98d4ac authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Fix typo.

parent 9e503f1a
...@@ -33,7 +33,7 @@ Section definitions. ...@@ -33,7 +33,7 @@ Section definitions.
| nsteps_O x : nsteps 0 x x | nsteps_O x : nsteps 0 x x
| nsteps_l n x y z : R x y nsteps n y z nsteps (S n) x z. | nsteps_l n x y z : R x y nsteps n y z nsteps (S n) x z.
(** Reduction of at most [n] steps. *) (** Reductions of at most [n] steps. *)
Inductive bsteps : nat relation A := Inductive bsteps : nat relation A :=
| bsteps_refl n x : bsteps n x x | bsteps_refl n x : bsteps n x x
| bsteps_l n x y z : R x y bsteps n y z bsteps (S n) x z. | bsteps_l n x y z : R x y bsteps n y z bsteps (S n) x z.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment