diff options
Diffstat (limited to 'stdlib/source/lux/math/constructive.lux')
| -rw-r--r-- | stdlib/source/lux/math/constructive.lux | 27 |
1 files changed, 15 insertions, 12 deletions
diff --git a/stdlib/source/lux/math/constructive.lux b/stdlib/source/lux/math/constructive.lux index 4cc1a839e..f9192bdee 100644 --- a/stdlib/source/lux/math/constructive.lux +++ b/stdlib/source/lux/math/constructive.lux @@ -33,7 +33,7 @@ (.|>> @representation)) ) -(syntax: #export (@ [name s.symbol]) +(syntax: #export (@ {name s.symbol}) (do @ [witnessT (macro.find-type name)] (.case (.<| (poly.run witnessT) @@ -47,8 +47,9 @@ (#e.Error error) (macro.fail error)))) -(syntax: #export (proof: [export? scr.export] - [name s.local-symbol] +(syntax: #export (proof: + {export? scr.export} + {name s.local-symbol} type proof) (do @ @@ -107,9 +108,10 @@ (s.Syntax [.Text (.List .Text)]) (s.form (p.seq s.local-symbol (p.many s.local-symbol)))) -(syntax: #export (proposition: [export? scr.export] - [[name elements] proposition-declaration] - [meaning (p.maybe s.any)]) +(syntax: #export (proposition: + {export? scr.export} + {[name elements] proposition-declaration} + {meaning (p.maybe s.any)}) (.case meaning #.None (wrap (.list (.` ((~! abstract:) (~+ (scw.export export?)) @@ -146,11 +148,11 @@ (.Ex [(~+ g!identities)] (-> (~+ g!requisites) (~ meaning))))))) -(syntax: #export (axiom [description (p.default "" s.text)]) +(syntax: #export (axiom {description (p.default "" s.text)}) (wrap (.list (.` (.:!! []))))) -(syntax: #export (theorem [type-vars type-vars] - [[name inputs] theorem-declaration] +(syntax: #export (theorem {type-vars type-vars} + {[name inputs] theorem-declaration} outputT meaning) (.let [inputs-names (list/map (.|>> input-name code.local-symbol) @@ -168,9 +170,10 @@ (#Anonymous [name type]) (.` [(~ (code.local-symbol name)) (~ type)]))) -(syntax: #export (theorem: [export? scr.export] - [type-vars type-vars] - [[name inputs] theorem-declaration] +(syntax: #export (theorem: + {export? scr.export} + {type-vars type-vars} + {[name inputs] theorem-declaration} outputT meaning) (wrap (.list (.` (..proof: (~+ (scw.export export?)) |