Mercurial > hg > Members > kono > Proof > FirstOrder

changeset 17:76e933149151

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 15 Aug 2020 17:15:14 +0900
parents fbecfa63dc2c
children 6cd5b63ecc38
files clausal.agda example2.agda
diffstat 2 files changed, 1 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/clausal.agda	Sat Aug 15 17:00:07 2020 +0900
+++ b/clausal.agda	Sat Aug 15 17:15:14 2020 +0900
@@ -50,7 +50,7 @@
    skolemv1 : (Statement → List Const → List Func → List Var → Statement )
              → Statement → List Const → List Func → List Var → Statement
    skolemv1 next (All x => s )   cl fl vl              = skolemv1 next s cl fl ( x ∷ vl) 
-   -- all existentical quantifiers are replaced by constants or funcions
+   -- all existential quantifiers are replaced by constants or funcions
    skolemv1 next (Exist x => s ) [] fl []              = skolemv1 next s [] fl [] 
    skolemv1 next (Exist x => s ) (sk ∷ cl ) fl []      = skolemv1 next (subst-prop s sbst x (Expr.const sk)) cl fl [] 
    skolemv1 next (Exist x => s ) cl [] (v ∷ t)         = skolemv1 next s cl [] (v ∷ t)
--- a/example2.agda	Sat Aug 15 17:00:07 2020 +0900
+++ b/example2.agda	Sat Aug 15 17:15:14 2020 +0900
@@ -14,7 +14,6 @@
       Z : Var
 
 data Func : Set where
-      f : Func
 
 data Pred : Set where
       father : Pred