Mercurial > hg > Members > kono > Proof > FirstOrder

comparison example1.agda @ 15:2f4db56bb289 current

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix example
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 15 Aug 2020 16:59:52 +0900
parents edf4a816abff
children 6cd5b63ecc38
comparison
equal deleted inserted replaced
14:1e3ebb348a54 15:2f4db56bb289
1 module example1 where 1 module example1 where
2 open import Data.List hiding (all ; and ; or ) 2 open import Data.List hiding (all ; and ; or )
3 open import Data.Maybe 3 open import Data.Maybe
4 open import Data.Bool hiding ( not ) 4 open import Data.Bool hiding ( not ; _∧_ ; _∨_ )
5 5
6 data Const : Set where 6 data Const : Set where
7 a : Const 7 a : Const
8 b : Const 8 b : Const
9 c : Const 9 c : Const
24 r : Pred 24 r : Pred
25 25
26 open import Logic Const Func Var Pred 26 open import Logic Const Func Var Pred
27 27
28 ex1 : Statement 28 ex1 : Statement
29 ex1 = ¬ ( pred q /\ ( All X => predx p ( func f (var X) ) )) 29 ex1 = ¬ ( pred q ∧ ( All X => predx p ( func f (var X) ) ))
30 30
31 subst-expr : Expr → Var → Expr → Expr 31 subst-expr : Expr → Var → Expr → Expr
32 subst-expr (var X) X v = v 32 subst-expr (var X) X v = v
33 subst-expr (var Y) Y v = v 33 subst-expr (var Y) Y v = v
34 subst-expr (var Z) Z v = v 34 subst-expr (var Z) Z v = v
49 all0 = const a ∷ const b ∷ const c ∷ [] 49 all0 = const a ∷ const b ∷ const c ∷ []
50 50
51 test003 : Bool 51 test003 : Bool
52 test003 = M amap pmap all0 subst-expr ( Exist X => predx p (var X) ) 52 test003 = M amap pmap all0 subst-expr ( Exist X => predx p (var X) )
53 53
54 open import clausal Const Func Var Pred
55
56 test004 : List Clause
57 test004 = translate ( Exist X => predx p (var X) ) (c ∷ []) (h ∷ []) subst-expr
58