test.txt

{
  "syntaxIdentical": false,
  "structurallyEqual": true,
  "size": 3,
  "proofTag": "alias",
  "members": [
    {
      "statement": "(motive : NameGenerator × NameGenerator → Sort u_1) →\n  (x : NameGenerator × NameGenerator) → ((cngen ngen : NameGenerator) → motive (cngen, ngen)) → motive x",
      "namespace": "_private.Lean.Meta.LazyDiscrTree.0.Lean.Meta.LazyDiscrTree.getChildNgen",
      "name": "_private.Lean.Meta.LazyDiscrTree.0.Lean.Meta.LazyDiscrTree.getChildNgen.match_1",
      "isRfl": false,
      "hasValue": true,
      "deprecated": false,
      "baseName": "match_1"
    },
    {
      "statement": "(motive : NameGenerator × NameGenerator → Sort u_1) →\n  (x : NameGenerator × NameGenerator) → ((cNGen ngen : NameGenerator) → motive (cNGen, ngen)) → motive x",
      "namespace": "_private.Mathlib.Lean.Meta.RefinedDiscrTree.0.Lean.Meta.RefinedDiscrTree.findImportMatches",
      "name": "_private.Mathlib.Lean.Meta.RefinedDiscrTree.0.Lean.Meta.RefinedDiscrTree.findImportMatches.match_3",
      "isRfl": false,
      "hasValue": true,
      "deprecated": false,
      "baseName": "match_3"
    },
    {
      "statement": "(motive : NameGenerator × NameGenerator → Sort u_1) →\n  (x : NameGenerator × NameGenerator) → ((cngen ngen : NameGenerator) → motive (cngen, ngen)) → motive x",
      "namespace": "_private.Mathlib.Lean.Meta.RefinedDiscrTree.Initialize.0.Lean.Meta.RefinedDiscrTree.getChildNgen",
      "name": "_private.Mathlib.Lean.Meta.RefinedDiscrTree.Initialize.0.Lean.Meta.RefinedDiscrTree.getChildNgen.match_1",
      "isRfl": false,
      "hasValue": true,
      "deprecated": false,
      "baseName": "match_1"
    }
  ],
  "groupId": 0,
  "fingerprint": 5707331
}