• Andrei Paskevich's avatar
    switch Typing to the new Dterm-based API · 460e93f8
    Andrei Paskevich authored
    Also:
    
    - Make [Highord.pred 'a] an alias for [Highord.func 'a bool],
    rename [Highorg.(@!)] to [(@)], remove [Highorg.(@?)], remove
    the quantifiers [\!] and [\?] and only leave [\] which is the
    only true lambda now;
    
    - Allow mixing bool and Prop in logic, Dterm will introduce
    coercions where necessary (trying to minimize the number of
    if-then-else in the term context).
    460e93f8
Name
Last commit
Last update
..
decl.ml Loading commit data...
decl.mli Loading commit data...
dterm.ml Loading commit data...
dterm.mli Loading commit data...
env.ml Loading commit data...
env.mli Loading commit data...
ident.ml Loading commit data...
ident.mli Loading commit data...
pattern.ml Loading commit data...
pattern.mli Loading commit data...
pretty.ml Loading commit data...
pretty.mli Loading commit data...
printer.ml Loading commit data...
printer.mli Loading commit data...
task.ml Loading commit data...
task.mli Loading commit data...
term.ml Loading commit data...
term.mli Loading commit data...
theory.ml Loading commit data...
theory.mli Loading commit data...
trans.ml Loading commit data...
trans.mli Loading commit data...
ty.ml Loading commit data...
ty.mli Loading commit data...