forked from GitHub/gf-core
added categoryProb, functionProb, functionIsConstructor
This commit is contained in:
@@ -2,10 +2,10 @@ abstract basic = {
|
||||
|
||||
cat N; S ;
|
||||
|
||||
fun z : N ;
|
||||
s : N -> N ;
|
||||
data z : N ;
|
||||
s : N -> N ;
|
||||
|
||||
fun c : N -> S ;
|
||||
data c : N -> S ;
|
||||
|
||||
cat P N ;
|
||||
fun ind : P z -> ((x:N) -> P x -> P (s x)) -> ((x : N) -> P x) ;
|
||||
|
||||
Reference in New Issue
Block a user