noah
/
morphexamples
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

formatting

This commit is contained in:
Noah Diewald 2021-06-04 03:01:48 -04:00
parent c1aaa36c72
commit 38d6fb8870
No known key found for this signature in database
GPG Key ID: EC2BAE1E100A5509
1 changed files with 5 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
Wao.v
View File

@ -161,7 +161,11 @@ Definition conjmeaning (α β : e → prop) : (e → prop) :=
Inductive meaning : sense → lₗ → mₘ → Prop :=
m₁ : ∀ s l m, m = baseₘ → In (l, s) lexmeaning → meaning s l m
| m₂ : ∀ (s₁ : e → prop) (s₂ : e → prop) l m, m = poₘ → In (l, existT Sns (func ent prp) s₁) lexmeaning → In (m, existT Sns (func ent prp) s₂) catmeaning → meaning (existT Sns (func ent prp) (conjmeaning s₁ s₂)) l m.
| m₂ : ∀ (s₁ : e → prop) (s₂ : e → prop) l m,
m = poₘ →
In (l, existT Sns (func ent prp) s₁) lexmeaning →
In (m, existT Sns (func ent prp) s₂) catmeaning →
meaning (existT Sns (func ent prp) (conjmeaning s₁ s₂)) l m.
(** A relation for providing proofs of lexical meanings. This is at
the proof of concept stage. *)