aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic
diff options
context:
space:
mode:
authorGravatar Tej Chajed <tchajed@mit.edu>2018-08-17 11:50:57 -0400
committerGravatar Tej Chajed <tchajed@mit.edu>2018-08-17 11:50:57 -0400
commit5c27e4a9398cb366e087594dd1c72e4c084fae01 (patch)
treecf24865ec0299070cf7d24af6a81cec9e0df98a7 /generic
parentb7f17b7ca09276be5cd29263bd5574fdd6fa4d2c (diff)
Support the Variant vernacular
Syntactically looks much like an Inductive, though it is non-recursive so "where" (mutual recursion) is not supported.
Diffstat (limited to 'generic')
0 files changed, 0 insertions, 0 deletions