935   \end{tabular}

   935   \end{tabular}

   936   \end{center}

   936   \end{center}

   937 

   937 

   938   \noindent

   938   \noindent

   939   Similarly for the other binding modes. Interestingly, in case of \isacommand{bind\_set}

   939   Similarly for the other binding modes. Interestingly, in case of \isacommand{bind\_set}

   942   show this later with an example.

   942   show this later with an example.

   943   

   943   

   944   There are some restrictions we need to impose on binding clasues: First, a

   944   There are some restrictions we need to impose on binding clasues: First, a

   945   body can only occur in \emph{one} binding clause of a term constructor. For

   945   body can only occur in \emph{one} binding clause of a term constructor. For

   946   binders we distinguish between \emph{shallow} and \emph{deep} binders.

   946   binders we distinguish between \emph{shallow} and \emph{deep} binders.

  1056   \noindent

  1056   \noindent

  1057   The difference is that with @{text Let} we only want to bind the atoms @{text

  1057   The difference is that with @{text Let} we only want to bind the atoms @{text

  1058   "bn(as)"} in the term @{text t}, but with @{text "Let_rec"} we also want to bind the atoms

  1058   "bn(as)"} in the term @{text t}, but with @{text "Let_rec"} we also want to bind the atoms

  1059   inside the assignment. This difference has consequences for the free-variable 

  1059   inside the assignment. This difference has consequences for the free-variable 

  1060   function and alpha-equivalence relation, which we are going to define below.

  1060   function and alpha-equivalence relation, which we are going to define below.

  1062   For this definition, we have to impose some restrictions on deep binders. First,

  1061   For this definition, we have to impose some restrictions on deep binders. First,

  1063   we cannot have more than one binding function for one binder. So we exclude:

  1062   we cannot have more than one binding function for one binder. So we exclude:

  1064 

  1063 

  1065   \begin{center}

  1064   \begin{center}

  1066   \begin{tabular}{ll}

  1065   \begin{tabular}{ll}