msyds/gf-core
1
0
Fork 0
forked from GitHub/gf-core
Code Pull Requests Activity

even simpler version of NQueens

Browse Source
This commit is contained in:
krasimir
2010-03-24 21:04:37 +00:00
parent ab3127b5dd
commit 69535e2b6b
4 changed files with 5 additions and 11 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
examples/nqueens/NQueens.gf
View File

@@ -6,7 +6,9 @@ cat Vec (s,l : Nat) Constr ;
cat Sat Nat Nat Constr ;
data nilV : (s : Nat) -> (c : Constr) -> Vec s zero c ;
consV : (s,l,j : Nat) -> (c : Constr) -> LT j s -> Sat j (succ zero) c -> Vec s l (consC j c) -> Vec s (succ l) c ;
consV : (l,j,k : Nat) ->
let s = succ (plus j k)
in (c : Constr) -> Sat j (succ zero) c -> Vec s l (consC j c) -> Vec s (succ l) c ;
nilC : Constr ;
consC : (j : Nat) -> Constr -> Constr ;