Changes
1 changed files (+0/-72)
-
Main copy.lean (deleted)
-
@@ -1,72 +0,0 @@import Std.Data abbrev TypeList := { αs : List Type // 0 < αs.length } def TypeList.toType : TypeList → Type | ⟨[α], _⟩ => α | ⟨α :: α' :: αs, _⟩ => α × TypeList.toType ⟨α' :: αs, by grind⟩ inductive DTerm (α : Type) | const (x : α) | var (s : String) def TypeList.toDTerms : TypeList → Type | ⟨[α], _⟩ => DTerm α | ⟨α :: α' :: αs, _⟩ => DTerm α × TypeList.toDTerms ⟨α' :: αs, by grind⟩ def Atom (relations : Std.HashMap String TypeList) := (rel : { rel : String // rel ∈ relations.keys }) × (relations[rel.val]'(by grind)).toDTerms def Rule (relations : Std.HashMap String TypeList) := Atom relations × List (Atom relations) def relations : Std.HashMap String TypeList := .ofList [ ("edge", ⟨[Nat, Nat], by decide⟩), ("path", ⟨[Nat, Nat], by decide⟩), ] theorem relEdge : relations["edge"]'(by simp [relations]) = ⟨[Nat, Nat], by decide⟩ := by simp [relations] grind theorem relPath : relations["path"]'(by simp [relations]) = ⟨[Nat, Nat], by decide⟩ := by simp [relations] grind def pathRule : Rule relations := by constructor · simp [Atom] constructor rotate_left · exact ⟨"path", by simp [relations]⟩ · simp rw [relPath] simp [TypeList.toDTerms] exact (.var "x", .var "y") -- : { rel // rel ∈ relations.keys }), (DTerm.var "x", DTerm.var "y")) -- (((⟨"path", by native_decide⟩ : { rel // rel ∈ relations.keys }), (DTerm.var "x", DTerm.var "y")), -- [ -- ((⟨"path", by native_decide⟩ : { rel // rel ∈ relations.keys }), (DTerm.var "y", DTerm.var "z")), -- ((⟨"edge", by native_decide⟩ : { rel // rel ∈ relations.keys }), (DTerm.var "x", DTerm.var "z")), -- ]) -- -- def Relation αs (h : 0 < αs.length := by grind) [BEq (ListToTypeTuple αs h)] [Hashable (ListToTypeTuple αs h)] := -- Std.HashSet (ListToTypeTuple αs h) -- def A : Relation [String, String] := .ofList [("hi", "blah")] -- def Rule (head : ) -- #eval A.contains ("hi", "blah") -- def main : IO Unit := -- IO.println s!"Hello!"
-