rule_name2.dk 112 Bytes
Newer Older
Guillaume GENESTIER's avatar
Guillaume GENESTIER committed
1 2 3 4 5 6 7 8
#NAME rule_name.

nat : Type.

0 : nat.

def plus : nat -> nat -> nat.

Gaspard FEREY's avatar
Gaspard FEREY committed
9
{rule_name.plus_0_n} [n] plus 0 n --> n.