Команда #check

Команда #check проверяет тип терма относительно заданного типа.

Синтаксис

#check <term> : <type>

Описание

Команда #check проверяет, что терм имеет указанный тип. Если проверка типов успешна, команда завершается без ошибки. Если она не удаётся, отображается сообщение об ошибке.

Пример

#lang rzk-1
#define id (A : U)
  : A → A
  := \ x → x

-- Проверить, что id имеет правильный тип
#check id : (A : U) → A → A

-- Проверить, что применение id к типу работает
#check id U : U → U

-- Проверить, что применение id к значению работает
#define unit-type
  : U
  := Unit
#check id unit-type unit : Unit