ext_json.v

Require Extraction.
(* https://coq.github.io/doc/master/stdlib/Coq.Arith.Factorial.html *)
Require Import Coq.Arith.Factorial.

Extraction Language JSON.
Extraction fact.
(*
{
  "what": "decl:fixgroup",
  "fixlist": [
    {
      "what": "fixgroup:item", "name": "fact",
      "type": {
        "what": "type:arrow",
        "left": {
          "what": "type:glob", "name": "nat", "args": [

          ]
        }, "right": {
          "what": "type:glob", "name": "nat", "args": [

          ]
        }
      },
      "value": {
        "what": "expr:lambda", "argnames": [
          "n"
        ],
        "body": {
          "what": "expr:case", "expr": {
            "what": "expr:rel", "name": "n"
          },
          "cases": [
            {
              "what": "case",
              "pat": {
                "what": "pat:constructor", "name": "O", "argnames": [

                ]
              },
              "body": {
                "what": "expr:constructor", "name": "S",
                "args": [
                  {
                    "what": "expr:constructor", "name": "O", "args": [

                    ]
                  }
                ]
              }
            },
            {
              "what": "case",
              "pat": {
                "what": "pat:constructor", "name": "S", "argnames": [
                  "n0"
                ]
              },
              "body": {
                "what": "expr:apply",
                "func": {
                  "what": "expr:global", "name": "mul"
                },
                "args": [
                  {
                    "what": "expr:constructor", "name": "S",
                    "args": [
                      {
                        "what": "expr:rel", "name": "n0"
                      }
                    ]
                  },
                  {
                    "what": "expr:apply",
                    "func": {
                      "what": "expr:global", "name": "fact"
                    }, "args": [
                      {
                        "what": "expr:rel", "name": "n0"
                      }
                    ]
                  }
                ]
              }
            }
          ]
        }
      }
    }
  ]
}
*)