Merge branch 'develop-remove-pragmas-theorem'. Close #613.

**Description**

The code of `copilot-theorem` contains unused language pragmas. To comply with
our coding style, which required unused code not to be included in the
codebase, those pragmas should be removed.

**Type**

- Management: comply with styling requirement.

**Additional context**

None.

**Requester**

- Ivan Perez.

**Method to check presence of bug**

Not applicable (not a bug).

**Expected result**

The code contains no unused pragmas. Running `hlint` with the following
auxiliary file indicates that there are no unused PRAGMAS.

```yaml
- ignore: {name: "Redundant bracket"}
- ignore: {name: "Use infix"}
- ignore: {name: "Redundant as"}
- ignore: {name: "Redundant <$>"}
- ignore: {name: "Use camelCase"}
- ignore: {name: "Avoid lambda"}
- ignore: {name: "Use gets"}
- ignore: {name: "Redundant $"}
- ignore: {name: "Use <&>"}
- ignore: {name: "Use concatMap"}
- ignore: {name: "Move brackets to avoid $"}
- ignore: {name: "Use /="}
- ignore: {name: "Use newtype instead of data"}
- ignore: {name: "Use :"}
- ignore: {name: "Replace case with fromMaybe"}
- ignore: {name: "Use >=>"}
- ignore: {name: "Use curry"}
- ignore: {name: "Use first"}
- ignore: {name: "Use hPrint"}
- ignore: {name: "Use or"}
- ignore: {name: "Use fmap"}
- ignore: {name: "Use if"}
- ignore: {name: "Use <$>"}
- ignore: {name: "Reduce duplication"}
- ignore: {name: "Eta reduce"}
```

The following dockerfile runs hlint on copilot-theorem with the provided list
of ignored warnings, which does not include unnecessary language pragmas, and
checks that there are no warnings reported, after which it prints the message
success:
```
--- Dockerfile-verify-613
FROM ubuntu:jammy

ENV DEBIAN_FRONTEND=noninteractive

RUN apt-get update

RUN apt-get install --yes git
RUN apt-get install --yes hlint

ADD ignore.yaml /tmp/ignore.yaml

RUN hlint --version

SHELL ["/bin/bash", "-c"]
CMD git clone $REPO \
    && cd $NAME \
    && git checkout $COMMIT \
    && hlint -h /tmp/ignore.yaml copilot-theorem/src \
    && echo "Success"

--- ignore.yaml
- ignore: {name: "Redundant bracket"}
- ignore: {name: "Use infix"}
- ignore: {name: "Redundant as"}
- ignore: {name: "Redundant <$>"}
- ignore: {name: "Use camelCase"}
- ignore: {name: "Avoid lambda"}
- ignore: {name: "Use gets"}
- ignore: {name: "Redundant $"}
- ignore: {name: "Use <&>"}
- ignore: {name: "Use concatMap"}
- ignore: {name: "Move brackets to avoid $"}
- ignore: {name: "Use /="}
- ignore: {name: "Use newtype instead of data"}
- ignore: {name: "Use :"}
- ignore: {name: "Replace case with fromMaybe"}
- ignore: {name: "Use >=>"}
- ignore: {name: "Use curry"}
- ignore: {name: "Use first"}
- ignore: {name: "Use hPrint"}
- ignore: {name: "Use or"}
- ignore: {name: "Use fmap"}
- ignore: {name: "Use if"}
- ignore: {name: "Use <$>"}
- ignore: {name: "Reduce duplication"}
- ignore: {name: "Eta reduce"}
```

Command (substitute variables based on new path after merge):
```
$ docker run -e "REPO=https://github.com/Copilot-Language/copilot" -e "NAME=copilot" -e "COMMIT=<HASH>" -it copilot-verify-613
```

**Solution implemented**

Remove all unused PRAGMAS from the code in `copilot-theorem`.

**Further notes**

None.

Author: ivanperez-keera

copilot-theorem/CHANGELOG

@@ -1,3 +1,6 @@
+2025-05-29
+        * Removed unused pragmas. (#613)
+
 2025-05-07
         * Version bump (4.4). (#618)
         * Translate quantifiers correctly in Kind2 backend. (#594)

copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs

@@ -1,4 +1,3 @@
-{-# LANGUAGE LambdaCase  #-}
 {-# LANGUAGE Trustworthy #-}
 
 -- | A prover backend based on Kind2.

copilot-theorem/src/Copilot/Theorem/Prover/SMTIO.hs

@@ -1,4 +1,3 @@
-{-# LANGUAGE LambdaCase     #-}
 {-# LANGUAGE NamedFieldPuns #-}
 {-# LANGUAGE RankNTypes     #-}
 {-# LANGUAGE Safe           #-}

copilot-theorem/src/Copilot/Theorem/What4.hs

@@ -1,18 +1,13 @@
-{-# LANGUAGE DataKinds                  #-}
-{-# LANGUAGE FlexibleContexts           #-}
-{-# LANGUAGE GADTs                      #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE KindSignatures             #-}
-{-# LANGUAGE LambdaCase                 #-}
-{-# LANGUAGE MultiWayIf                 #-}
-{-# LANGUAGE PatternSynonyms            #-}
-{-# LANGUAGE RankNTypes                 #-}
-{-# LANGUAGE ScopedTypeVariables        #-}
-{-# LANGUAGE StandaloneDeriving         #-}
-{-# LANGUAGE TemplateHaskell            #-}
-{-# LANGUAGE TupleSections              #-}
-{-# LANGUAGE TypeApplications           #-}
-{-# LANGUAGE TypeOperators              #-}
+{-# LANGUAGE DataKinds           #-}
+{-# LANGUAGE FlexibleContexts    #-}
+{-# LANGUAGE GADTs               #-}
+{-# LANGUAGE KindSignatures      #-}
+{-# LANGUAGE LambdaCase          #-}
+{-# LANGUAGE PatternSynonyms     #-}
+{-# LANGUAGE RankNTypes          #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications    #-}
+{-# LANGUAGE TypeOperators       #-}
 
 -- |
 -- Module      : Copilot.Theorem.What4