Convert a Variables to two Admitted statements

[arnoudvanderleer]

in a Birmingham 2017 exercise set, to make the CI compile again with coq 8.20 and above

[benediktahrens]

I think a slightly better solution would be to put the Variables in a section? Using Variable signals that we consider those things variables, or hypotheses. Using Admitted might make one think that these are things that should be proved?

[arnoudvanderleer]

Generally, this is true. However, in this case, the context of these variables was

(* FILL IN THE DEFINITIONS OF istrans AND issymm *)
(* Definition istrans {X : UU} (R : hrel X) : UU := *)
(* Definition issymm {X : UU} (R : hrel X) : UU := *)
Variables istrans issymm: forall {X: UU}, hrel X -> UU. (* to be deleted *)

So I think these actually were supposed to be proved (or constructed)

[benediktahrens]

I think it is the types that are to be defined as an exercise, but not terms of those types?

[arnoudvanderleer]

The types of istrans and issymm are already filled in here, right? They are just forall {X : UU}, hrelX -> UU. And why would it say to be deleted in the comment after Variables, and are there two commented Definition statements, if these things are supposed to be variables?

[arnoudvanderleer]

The corresponding part in the 2024-Minneapolis exercises is

(** ** Definitions *)

Definition hrel (X : UU) : UU := X -> X -> hProp.

Definition isrefl {X : UU} (R : hrel X) : UU
  := ∏ x : X, R x x.
Definition istrans {X : UU} (R : hrel X) : UU := fill_me.
Definition issymm {X : UU} (R : hrel X) : UU := fill_me.

Definition ispreorder {X : UU} (R : hrel X) : UU := istrans R × isrefl R.

[benediktahrens]

@arnoudvanderleer : sorry, I had misread the code! This looks good, I'll merge.