diff options
Diffstat (limited to 'test/golden/datatype/tokenizing.golden')
| -rw-r--r-- | test/golden/datatype/tokenizing.golden | 45 |
1 files changed, 45 insertions, 0 deletions
diff --git a/test/golden/datatype/tokenizing.golden b/test/golden/datatype/tokenizing.golden index 1827a62..90f8274 100644 --- a/test/golden/datatype/tokenizing.golden +++ b/test/golden/datatype/tokenizing.golden @@ -73,6 +73,15 @@ , EndEnv "proposition" ] , + [ BeginEnv "proof" + , Word "follows" + , Word "by" + , Ref + ( "propform_propbot_intro" :| [] ) + , Symbol "." + , EndEnv "proof" + ] +, [ BeginEnv "proposition" , Label "propform_var_test" , Word "if" @@ -97,6 +106,15 @@ , EndEnv "proposition" ] , + [ BeginEnv "proof" + , Word "follows" + , Word "by" + , Ref + ( "propform_propvar_intro" :| [] ) + , Symbol "." + , EndEnv "proof" + ] +, [ BeginEnv "proposition" , Label "propform_imp_test" , BeginEnv "math" @@ -112,6 +130,15 @@ , EndEnv "proposition" ] , + [ BeginEnv "proof" + , Word "follows" + , Word "by" + , Ref + ( "propform_propbot_intro" :| [ "propform_propto_intro" ] ) + , Symbol "." + , EndEnv "proof" + ] +, [ BeginEnv "proposition" , Label "propform_distinct_test" , BeginEnv "math" @@ -127,6 +154,15 @@ , EndEnv "proposition" ] , + [ BeginEnv "proof" + , Word "follows" + , Word "by" + , Ref + ( "propform_propbot_propto_distinct" :| [] ) + , Symbol "." + , EndEnv "proof" + ] +, [ BeginEnv "proposition" , Label "propform_injective_test" , Word "if" @@ -151,4 +187,13 @@ , Symbol "." , EndEnv "proposition" ] +, + [ BeginEnv "proof" + , Word "follows" + , Word "by" + , Ref + ( "propform_propvar_injective" :| [] ) + , Symbol "." + , EndEnv "proof" + ] ]
\ No newline at end of file |