The demo Plugin

Table of Contents

• Operations
  • %demo.const_idx

See also

mim::plug::demo

A minimal demo plugin.

Operations

%demo.const_idx

The constant 42, evaluated by a normalizer.

axm %demo.const_idx: [n: Nat] → Idx n, normalize_const;