- initial support for abstractions with explicit levels

[helm.git] / helm / software / lambda-delta / src / text / txtLexer.mll

diff --git a/helm/software/lambda-delta/src/text/txtLexer.mll b/helm/software/lambda-delta/src/text/txtLexer.mll
index e5ced380684b07046560d3a49e341c67432a1937..efee66051904cef4606a3dba1c687aaf3cab2b1e 100644 (file)
--- a/helm/software/lambda-delta/src/text/txtLexer.mll
+++ b/helm/software/lambda-delta/src/text/txtLexer.mll
@@ -46,6 +46,7 @@ and token = parse
    | "\\graph"    { out "GRAPH"; TP.GRAPH }
    | "\\decl"     { out "DECL"; TP.DECL   }
    | "\\ax"       { out "AX"; TP.AX       }
+   | "\\cong"     { out "CONG"; TP.CONG   }
    | "\\def"      { out "DEF"; TP.DEF     }
    | "\\th"       { out "TH"; TP.TH       }
    | "\\generate" { out "GEN"; TP.GEN     }
@@ -69,4 +70,5 @@ and token = parse
    | "~"          { out "TE"; TP.TE       }
    | "->"         { out "WTO"; TP.WTO     }
    | "=>"         { out "STO"; TP.STO     }
+   | "^"          { out "CT"; TP.CT       }
    | eof          { out "EOF"; TP.EOF     }