Patterns of terms/judgments/theorems in a Twelf file

sorts.elf

%Rob Simmons (he) (F2'23)
%9:12 AM
%Patterns of terms/judgments/theorems in a Twelf file

nat: type.           % pattern is "a0 : k0"
z: nat.              % pattern is "c0 : tau"
s: nat -> nat.       % pattern is "c0 : tau"
two : nat = s (s z). % pattern is "c0 : tau = t"

plus : nat -> nat -> nat -> type. % pattern is "a1 : k1"
plus/z : plus z N N.              % pattern is "c1 : A"
plus/s : plus N M P -> plus (s N) M (s P).
                              % pattern is "c1 : A"
plus123 : plus (s z) (s (s z)) (s (s (s z))) =
        plus/s plus/z.            % pattern is "c1 : A = M"

plusz : {N : nat} plus N z N -> type. % pattern is "a2 : k2"
plusz/z : plusz z plus/z.             % pattern is "c2 : T"
plusz/s : plusz (s N) (plus/s D)      % pattern is "c2 : T"
   <- plusz N D.

%mode plusz +N -D.
%worlds () (plusz _ _).
%total N (plusz N _).