"pred" is printed strangely
This code:
From stdpp Require Import prelude.
Check pred.
prints
Init.Nat.pred
: nat → nat
Looks like the pred
in scope is actually some parsing-only notation or so?
This code:
From stdpp Require Import prelude.
Check pred.
prints
Init.Nat.pred
: nat → nat
Looks like the pred
in scope is actually some parsing-only notation or so?