title: What does fun keyword do in Coq?
body: <p>I am struggling to understand the meaning of keyword 'fun' in Coq.</p>
  
  <p>There are types all and function forallb:</p>
  
  <pre><code>Inductive all (X : Type) (P : X -&gt; Prop) : list X -&gt; Prop :=
    | all_nil : all X P []
    | all_cons : forall (x:X) (l: list X) , P x -&gt; all X P l -&gt; all X P (x::l).
  
  Fixpoint forallb {X : Type} (test : X -&gt; bool) (l : list X) : bool :=
   match l with
  | [] =&gt; true
  | x :: l' =&gt; andb (test x) (forallb test l')
  end.
  </code></pre>
  
  <p>And theorem:</p>
  
  <pre><code>Theorem all_spec: forall (X:Type) (test : X -&gt; bool) (l: list X),
      forallb test l = true &lt;-&gt; all X (fun x =&gt; test x = true) l.
  </code></pre>
  
  <p>I understand the left part but confused on what fun is doing on the right side of the &lt;->.</p>