Search for blocks/addresses/...
Proofgold Object
nat_primrec
1
(
λ x0 .
mul_nat
(
ordsucc
x0
)
)
type
ι
→
ι
theory
HotG
name
nat_factorial
definition
PUfRN..
Megalodon
nat_factorial
proofgold address
TMYee..
nat_factorial
creator
4972
Pr6Pc..
/
8c3a3..
owner
4972
Pr6Pc..
/
8c3a3..
term root
ff333..