diff --git a/source/test.mmt b/source/test.mmt index 3b3fa88109a354940a4cbed8b64ff0273bc3da67..37dd630527d164cd8d705bf2216501300da5278b 100644 --- a/source/test.mmt +++ b/source/test.mmt @@ -22,7 +22,7 @@ theory Basics = theory Pi : ?Basics = pi # { V1T ,… } 2 prec -10000 â™ - arrow # 1⟶… prec -9999 â™ + arrow # 1→… prec -9999 â™ apply1 # 1%w… prec -10 â™ apply2 # 1 ( 2,… ) prec -100000 â™ lambda # [ V1T ,… ] 2 prec -10000 â™ @@ -80,10 +80,10 @@ theory Mod : ?Basics = theory Term : ?Basics = // copy paste â™ - formation # {| 1 |} 2 prec -10000 - reflect # ⌜ 1 : 2 ⌠prec -10000 - eval # ⌞ 1 ⌟ 2 prec -10000 - elim # 1 ^ 2 prec -10000 + formation # {| 1 |} 2 prec -10000â™ + reflect # ⌜ 1 : 2 ⌠prec -10000â™ + eval # ⌞ 1 ⌟ 2 prec -10000â™ + elim # 1 ^ 2 prec -10000â™ âš theory FiniteSet : ?Basics = @@ -108,7 +108,7 @@ theory MultiSet : ?Basics = theory InfiniteSequences : ?Basics = // pretty much identical to finite sequences, notationwise. Probably additional introduction - form via â„• ⟶ A or induction? â™ + form via â„• → A or induction? â™ infseq # 1 ^≤ω â™ nil # nil %I1 â™ cons # 1 :: 2 â™