diff options
Diffstat (limited to '')
| -rw-r--r-- | stdlib/source/lux/math/constructive.lux | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/stdlib/source/lux/math/constructive.lux b/stdlib/source/lux/math/constructive.lux index 762e15e31..c360a0552 100644 --- a/stdlib/source/lux/math/constructive.lux +++ b/stdlib/source/lux/math/constructive.lux @@ -133,7 +133,7 @@ g!identities (.|> inputs (list.filter identified?) (list/map (.|>> input-name code.local-symbol))) - g!requisites (list/map (.function [input] + g!requisites (list/map (.function (_ input) (.case input (#Identified input') (.` (..Witness (~ (.get@ #input-type input')) @@ -156,8 +156,7 @@ (.let [inputs-names (list/map (.|>> input-name code.local-symbol) inputs)] (wrap (.list (.` (.: (~ (theorem-type type-vars inputs outputT)) - (.function (~ (code.local-symbol name)) - [(~+ inputs-names)] + (.function ((~ (code.local-symbol name)) (~+ inputs-names)) (~ meaning)))))))) (.def: (input-code input) @@ -193,5 +192,5 @@ (.def: #export absurdity (.All [p] (-> p .Bottom)) - (.function [proof] + (.function (_ proof) (.error! (ex.construct Absurdity [])))) |