@edwinbrady Would it make sense to allow for "total" to appear in negative positions? E.g.,
total h : (total f : Nat -> Nat) -> Nat -> Nat
@dblhelix Probably not the way things currently work. Here, h may be total, but applications might not be if the f argument isn't.
-
-
@edwinbrady I see. I was considering it in the context of data-constructor types. Proof-carrying records à la Agda, explicit dictionaries...Thanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.