The natural number eliminator needs to be implemented. See the definition of the syntax Definition 4.1 "Syntax of Grady" and the definition of its typing rule in Figure 6 "Typing rules for Grady", and the definition of its evaluation rules in Figure 7 "Reduction rules for Grady"
The natural number eliminator needs to be implemented. See the definition of the syntax Definition 4.1 "Syntax of Grady" and the definition of its typing rule in Figure 6 "Typing rules for Grady", and the definition of its evaluation rules in Figure 7 "Reduction rules for Grady"