Coq Checker

Vand ID: vand-b873d708-5135-4520-a860-8b06b413eb41

Learn how to easily use the Coq Checker tool with the OpenAI API.

Check Coq code.

OpenAI function calls:

{
  "name": "coqc",
  "description": "Check Coq code using coqc. Don\u0027t forget to put all the context. Also, you can use Search to find relevant lemmas that you can use in your proofs.",
  "parameters": {
    "type": "object",
    "properties": {
      "v": {
        "type": "string",
        "description": "The Coq code to check."
      }
    },
    "required": [
      "v"
    ]
  }
}

Auth Type

none

Servers

https://coq-chatgpt.livecode.ch

OpenAPI:

{
  "openapi": "3.0.1",
  "info": {
    "title": "Coq Checker",
    "description": "Check Coq code.",
    "version": "v1"
  },
  "servers": [
    {
      "url": "https://coq-chatgpt.livecode.ch"
    }
  ],
  "paths": {
    "/coqc": {
      "post": {
        "operationId": "coqc",
        "summary": "Check Coq code using coqc. Don\u0027t forget to put all the context. Also, you can use Search to find relevant lemmas that you can use in your proofs.",
        "requestBody": {
          "required": true,
          "content": {
            "application/json": {
              "schema": {
                "$ref": "#/components/schemas/getCoqcRequest"
              }
            }
          }
        },
        "responses": {
          "200": {
            "description": "OK",
            "content": {
              "application/json": {
                "schema": {
                  "$ref": "#/components/schemas/getCoqcResponse"
                }
              }
            }
          }
        }
      }
    }
  },
  "components": {
    "schemas": {
      "getCoqcResponse": {
        "type": "object",
        "properties": {
          "log": {
            "type": "string",
            "description": "Error log."
          },
          "out": {
            "type": "string",
            "description": "Standard out log."
          },
          "status": {
            "type": "string",
            "description": "Status code."
          },
          "details": {
            "type": "string",
            "description": "Details of interaction in case of error, showing the last goal context. These details can be used for diagnostic."
          },
          "hint": {
            "type": "string",
            "description": "In case of error, a hint about how to fix the issue."
          },
          "context": {
            "type": "string",
            "description": "In case of error, gives the context in the script where the error occurred."
          }
        }
      },
      "getCoqcRequest": {
        "type": "object",
        "required": [
          "v"
        ],
        "properties": {
          "v": {
            "type": "string",
            "description": "The Coq code to check.",
            "required": true
          }
        }
      }
    }
  }
}