Defining mutually recursvie judgments/meta-functions

[mbuszka]

Is it possible to define mutually recursive judgements/meta-functions?

[rfindler]

Yes. This works, for example:

#lang racket
(require redex/reduction-semantics)

(define-language L
  (n ::= Z (S n)))

(define-judgment-form L
  #:mode (odd I)

  [(even n)
   ----------
   (odd (S n))])

(define-judgment-form L
  #:mode (even I)

  [--------
   (even Z)]

  [(odd n)
   ------------
   (even (S n))])

(test-judgment-holds (even Z))
(test-judgment-holds (odd (S Z)))
(test-judgment-holds (even (S (S Z))))
(test-equal (judgment-holds (odd Z)) #f)
(test-equal (judgment-holds (even (S Z))) #f)
(test-results)

[mbuszka]

Thank you!