HOcore.Prelim

Require Export Relations.Relations
               Program.Basics.

Require Export Base.Base.

Require Export Autosubst.Autosubst.

This file contains preliminary definitions and is included in every other file of the development

Modifications


Global Set Implicit Arguments.
Global Unset Strict Implicit.

(* Function composition *)
Notation " x °° y " := (compose x y) (at level 69, right associativity).

(* Make type argument implicit *)
Arguments reflexive [A] R.
Arguments symmetric [A] R.
Arguments transitive [A] R.
Arguments antisymmetric [A] R.
Arguments transp [A] R x y.

Preliminary Definitions / Lemmas


(* Notation as used in Paco Library (http://plv.mpi-sws.org/paco/)
     Relation inclusion:             "<2="
     Binary relation union operator: "\2/" *)


Notation "p <2= q" := (forall x0 x1 (PR : p x0 x1 : Prop), q x0 x1 : Prop) (at level 50, no associativity).
Notation "p \2/ q" := (fun x0 x1 => p x0 x1 \/ q x0 x1) (at level 50, no associativity).

(* Empty and unversal relations *)
Notation bot2 := (fun _ _ => False).
Notation top2 := (fun _ _ => True).