Команды #compute

Эти команды вычисляют термы до нормальной или слабой головной нормальной формы.

Синтаксис

#compute <term>
#compute-whnf <term>
#compute-nf <term>

Описание

• #compute <term> — псевдоним для #compute-whnf, вычисляет слабую головную нормальную форму (WHNF) терма
• #compute-whnf <term> — вычисляет слабую головную нормальную форму (WHNF) терма
• #compute-nf <term> — вычисляет полную нормальную форму (NF) терма

Эти команды полезны для отладки и понимания того, как вычисляются термы. Вычисленная форма выводится во время проверки типов.

Пример

#lang rzk-1
#define add (x y : Unit)
  : Unit
  := unit

#define double (x : Unit)
  : Unit
  := add x x

-- Вычислить слабую головную нормальную форму
#compute-whnf double unit
-- Вывод: unit

-- Вычислить полную нормальную форму
#compute-nf double unit
-- Вывод: unit