Open tchajed opened 1 year ago
It's now possible to (unsoundly) disable the positivity check, so the example can use an otherwise-ordinary inductive definition rather than a set of axioms.
It's now possible to (unsoundly) disable the positivity check, so the example can use an otherwise-ordinary inductive definition rather than a set of axioms.