5392def syntaxArithmeticHead =
5393 (lambda unrestricted syntax : (family Syntax) .
5394 (eliminate
5395 Syntax
5396 (lambda unrestricted current : (family Syntax) . Nat)
5397 syntax
5398 (branch SyntaxAtom spelling origin . zero)
5399 (branch SyntaxEmpty . zero)
5400 (branch SyntaxCons head tail ih_head ih_tail . (syntaxAtomIsArithmetic head))
5401 (branch SyntaxNode children ih_children . zero)))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.