# Definition of InLeft and InRight

So in reading I have come across the terms "InLeft" and "InRight" and I am unable to find a concrete definition for it.

I have found it used in the specification for COQ, and in some notes on compilers (there it was refered to as INL and INR).

As far as I am able to ascertain it is to do with making a difference between two options. However the seems like a weird nomenclature for something so simple.

The page you reference for Coq defines inLeft and inRight as constructors of the inductive type sumor. The names themselves come from "left/right injection", as in the left/right injection into a sum type. Other names commonly used are inl/inr, Left/Right, $\iota_0$/$\iota_1$, and variations on these (e.g. that Coq file also defines left/right in the definition of sumbool). It also defines inl/inr as the constructors of the general sum type. sum, sumor, and sumbool are minor, technical variations of each other.