mgql/MGQL.lean at main · EngineeringSoftware/mgql · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
/-
  MGQL: A Machine-Checked, Executable Semantics for a
  fragment of the ISO Graph Query Language

  Mechanized in Lean 4.
-/

import MGQL.Sorts
import MGQL.Syntax
import MGQL.Values
import MGQL.Schema
import MGQL.RecordSchema
import MGQL.Subtyping
import MGQL.Typing
import MGQL.Semantics
import MGQL.Metatheory
import MGQL.SmallStep
import MGQL.TypeChecker
import MGQL.LDBCBench
import MGQL.Test
import MGQL.Examples