- core_notation: bug fix in the input notation for congruent: we added term 90 after \sub
- library/nat/permutation.ma: added input notation for transpose and fixed term precedence in its output notation
- library/Makefile: compilation of single files re-enabled.
The syntax for compiling file.ma is is "make file.mo" and "make file.mo.opt"
now nat/congruence.ma and nat/permutation.ma are fully reconstructed :)
let children' = List.map aux_mpres children in
(fun size -> render_row size false children')
| Pres.Mfrac (_, m, n) ->
let children' = List.map aux_mpres children in
(fun size -> render_row size false children')
| Pres.Mfrac (_, m, n) ->
- aux_mpres (mrow [ text " \\frac "; parentesize m ; parentesize n])
- | Pres.Msqrt (_, m) -> aux_mpres (mrow [ text " \\sqrt "; parentesize m; ])
+ aux_mpres (mrow [ text " \\frac "; parentesize m ; text " "; parentesize n; text " " ])
+ | Pres.Msqrt (_, m) -> aux_mpres (mrow [ text " \\sqrt "; parentesize m; text " "])
| Pres.Mroot (_, r, i) ->
aux_mpres (mrow [
| Pres.Mroot (_, r, i) ->
aux_mpres (mrow [
- text " \\root "; parentesize i; text " \\of "; parentesize r ])
+ text " \\root "; parentesize i; text " \\of "; parentesize r; text " " ])
| Pres.Mstyle (_, m)
| Pres.Merror (_, m)
| Pres.Mpadded (_, m)
| Pres.Mstyle (_, m)
| Pres.Merror (_, m)
| Pres.Mpadded (_, m)
| Pres.Mfenced (_, children) -> aux_mpres (mrow children)
| Pres.Maction (_, []) -> assert false
| Pres.Msub (_, m, n) ->
| Pres.Mfenced (_, children) -> aux_mpres (mrow children)
| Pres.Maction (_, []) -> assert false
| Pres.Msub (_, m, n) ->
- aux_mpres (mrow [ parentesize m; text " \\sub "; parentesize n ])
+ aux_mpres (mrow [ text " "; parentesize m; text " \\sub "; parentesize n; text " " ])
- aux_mpres (mrow [ parentesize m; text " \\sup "; parentesize n ])
+ aux_mpres (mrow [ text " "; parentesize m; text " \\sup "; parentesize n; text " " ])
| Pres.Munder (_, m, n) ->
| Pres.Munder (_, m, n) ->
- aux_mpres (mrow [ parentesize m; text " \\below "; parentesize n ])
+ aux_mpres (mrow [ text " "; parentesize m; text " \\below "; parentesize n; text " " ])
| Pres.Mover (_, m, n) ->
| Pres.Mover (_, m, n) ->
- aux_mpres (mrow [ parentesize m; text " \\above "; parentesize n ])
+ aux_mpres (mrow [ text " "; parentesize m; text " \\above "; parentesize n; text " " ])
| Pres.Msubsup _
| Pres.Munderover _
| Pres.Mtable _ ->
| Pres.Msubsup _
| Pres.Munderover _
| Pres.Mtable _ ->
non associative with precedence 45
for @{ 'eq $t $a $b }.
non associative with precedence 45
for @{ 'eq $t $a $b }.
-notation > "hvbox(n break (≅ \sub p) m)"
+notation > "hvbox(n break (≅ \sub term 90 p) m)"
non associative with precedence 45
for @{ 'congruent $n $m $p }.
non associative with precedence 45
for @{ 'congruent $n $m $p }.
../matitadep -dot
depend.opt:
../matitadep.opt -dot
../matitadep -dot
depend.opt:
../matitadep.opt -dot
+
+%.mo:
+ ../matitac $*.ma
+%.mo.opt:
+ ../matitac.opt $*.ma
[ true \Rightarrow i
| false \Rightarrow n]].
[ true \Rightarrow i
| false \Rightarrow n]].
-notation < "(❲i↹j❳)n" with precedence 71
+notation < "(❲i↹j❳) term 72 n" with precedence 71
for @{ 'transposition $i $j $n}.
for @{ 'transposition $i $j $n}.
-notation < "(❲i \atop j❳)n" with precedence 71
+notation < "(❲i \atop j❳) term 72 n" with precedence 71
+for @{ 'transposition $i $j $n}.
+
+notation > "(❲\frac term 90 i term 90 j❳)n" with precedence 71
for @{ 'transposition $i $j $n}.
interpretation "natural transposition" 'transposition i j n = (transpose i j n).
for @{ 'transposition $i $j $n}.
interpretation "natural transposition" 'transposition i j n = (transpose i j n).
-qed.
\ No newline at end of file