aboutsummaryrefslogtreecommitdiffstats
path: root/SocietyCulture.lean
diff options
context:
space:
mode:
authorPetri Hienonen <petri.hienonen@gmail.com>2026-02-15 16:01:38 +0200
committerPetri Hienonen <petri.hienonen@gmail.com>2026-02-15 16:01:38 +0200
commit0f27a15749bd047912f09469653a83238f86ea0a (patch)
treed3f6c8ffc643160bf98c6703510326b6ea729f67 /SocietyCulture.lean
parent8ebc1b0ebb7244f73ace1407ccb672a151c3a052 (diff)
downloadkb-0f27a15749bd047912f09469653a83238f86ea0a.tar.zst
Remove
Diffstat (limited to 'SocietyCulture.lean')
-rw-r--r--SocietyCulture.lean17
1 files changed, 0 insertions, 17 deletions
diff --git a/SocietyCulture.lean b/SocietyCulture.lean
deleted file mode 100644
index ca4d0da..0000000
--- a/SocietyCulture.lean
+++ /dev/null
@@ -1,17 +0,0 @@
-import Mathematics
-
--- Knowledge Base domain: SocietyCulture
-
-opaque Person : Type
--- Person extends Entity
-axiom Person.val : Person → Entity
-opaque Place : Type
--- Place extends Entity
-axiom Place.val : Place → Entity
-opaque City : Type
--- City extends Place
-axiom City.val : City → Place
-opaque athens : City
-opaque birthyear : Person → Nat
-opaque bornIn : Person → Place → Prop
-axiom fact_bornIn_socrates_athens : bornIn socrates athens