WhoCites
Definitions
mb
hybrid
Sections
GenAutomata
Doc
Who Cites primrec?
primrec
Def primrec(n;b;c) == if n=
0
b else c(n-1,primrec(n-1;b;c)) fi (recursive)
Thm*
T:Type, n:
, b:T, c:(
n
T
T). primrec(n;b;c)
T
eq_int
Def
i=
j == if i=j
true
; false
fi
Thm*
i,j:
. (i=
j)
Syntax:
primrec(n;b;c)
has structure:
primrec(n; b; c)
About:
WhoCites
Definitions
mb
hybrid
Sections
GenAutomata
Doc