Mercurial > urweb
annotate demo/more/decision.urs @ 1034:a779402841f6
Hooks for measuring how much interesting proving is going on in elaboration
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 17 Nov 2009 12:44:14 -0500 |
| parents | 5d9f47124c4c |
| children |
| rev | line source |
|---|---|
| adamc@1030 | 1 val decision : Meta.private (option bool) |
| adamc@1030 | 2 |
| adamc@1030 | 3 functor Make (M : sig |
| adamc@1030 | 4 con paperOther :: {Type} |
| adamc@1030 | 5 constraint [Id, Decision] ~ paperOther |
| adamc@1030 | 6 include Conference.INPUT |
| adamc@1030 | 7 where con paper = [Decision = option bool] ++ paperOther |
| adamc@1031 | 8 |
| adamc@1032 | 9 val status : ctx ::: {Unit} -> [[Body] ~ ctx] => $([Id = paperId] ++ paperOther) |
| adamc@1032 | 10 -> transaction (xml ([Body] ++ ctx) [] []) |
| adamc@1030 | 11 end) : Conference.OUTPUT where con paper = [Decision = option bool] ++ M.paperOther |
| adamc@1030 | 12 where con userId = M.userId |
| adamc@1030 | 13 where con paperId = M.paperId |
| adamc@1030 | 14 where con yourPaperTables = [] |