max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/lean/PPRoundtrip.lean.expected.out
Leonardo de Moura 947369b4ce chore: Parenthesizer issues after removing sortApp 
@Kha Could you please double check these modifications.

I added a no-op for `checkRbpLt`. It is used at the `Sort` and `Type`
parsers.
As I described in previous commits, the `checkRBPGreater` comment and
implementation were misleading. It was actually succeeding when the
rbp was less than or equal to the given parameter. So, it was renamed
to `checkRbpLe`. So, is the depArrow parenthesizer ok? I did not check.

I updated the PPRoundtrip.lean.expected.out to make sure the tests
succeed, but we should revise it if there is a problem with the
modifications at Parenthesizer.lean
2020-06-03 15:46:33 -07:00

142 lines
4.7 KiB
Text
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

(Term.prop "Prop")
(Term.type "Type" (null))
(Term.type "Type" (null))
(Term.type "Type" (null (Level.num (numLit "1"))))
(Term.type "Type" (null (Level.hole "_")))
(Term.type "Type" (null (Level.paren "(" (Level.addLit (Level.hole "_") "+" (numLit "2")) ")")))
(Term.id `Nat (null))
(Term.app (Term.id `List (null)) (null (Term.id `Nat (null))))
(Term.app (Term.id `id (null)) (null (Term.id `Nat (null))))
(Term.app
(Term.id `id (null))
(null
(Term.paren
"("
(null
(Term.app
(Term.id `id (null))
(null (Term.paren "(" (null (Term.app (Term.id `id (null)) (null (Term.id `Nat (null)))) (null)) ")")))
(null))
")")))
(Term.app (Term.id `List (null)) (null (Term.id `Nat (null))))
(Term.app (Term.explicit "@" (Term.id `id (null))) (null (Term.type "Type" (null)) (Term.id `Nat (null))))
(Term.app
(Term.id `List (null (Term.explicitUniv ".{" (null (Level.num (numLit "0"))) "}")))
(null (Term.id `Nat (null))))
(Term.app
(Term.id `id (null (Term.explicitUniv ".{" (null (Level.num (numLit "2"))) "}")))
(null (Term.id `Nat (null))))
(Term.app
(Term.id `id (null))
(null
(Term.paren
"("
(null (Term.app (Term.explicit "@" (Term.id `id (null))) (null (Term.type "Type" (null)) (Term.id `Nat (null)))) (null))
")")))
(Term.fun
"fun"
(null (Term.paren "(" (null (Term.id `a (null)) (null (Term.typeAscription ":" (Term.id `Nat (null))))) ")"))
"=>"
(Term.id `a (null)))
(Term.fun
"fun"
(null
(Term.paren
"("
(null (Term.app (Term.id `a (null)) (null (Term.id `b (null)))) (null (Term.typeAscription ":" (Term.id `Nat (null)))))
")"))
"=>"
(Term.id `a (null)))
(Term.fun
"fun"
(null
(Term.paren "(" (null (Term.id `a (null)) (null (Term.typeAscription ":" (Term.id `Nat (null))))) ")")
(Term.paren "(" (null (Term.id `b (null)) (null (Term.typeAscription ":" (Term.id `Bool (null))))) ")"))
"=>"
(Term.id `a (null)))
(Term.fun
"fun"
(null (Term.implicitBinder "{" (null `a `b) (null ":" (Term.id `Nat (null))) "}"))
"=>"
(Term.id `a (null)))
(Term.app
(Term.id `typeAs (null))
(null
(Term.paren
"("
(null
(Term.depArrow
(Term.implicitBinder "{" (null `α) (null ":" (Term.type "Type" (null))) "}")
"→"
(Term.arrow (Term.id `α (null)) "→" (Term.id `α (null))))
(null))
")")
(Term.paren
"("
(null
(Term.fun
"fun"
(null
(Term.implicitBinder "{" (null `α) (null ":" (Term.type "Type" (null))) "}")
(Term.paren "(" (null (Term.id `a (null)) (null (Term.typeAscription ":" (Term.id `α (null))))) ")"))
"=>"
(Term.id `a (null)))
(null))
")")))
(Term.fun
"fun"
(null
(Term.implicitBinder "{" (null `α) (null ":" (Term.type "Type" (null))) "}")
(Term.instBinder "[" (null `_inst_1 ":") (Term.app (Term.id `HasToString (null)) (null (Term.id `α (null)))) "]")
(Term.paren "(" (null (Term.id `a (null)) (null (Term.typeAscription ":" (Term.id `α (null))))) ")"))
"=>"
(Term.app
(Term.explicit "@" (Term.id `HasToString.toString (null)))
(null (Term.id `α (null)) (Term.id `_inst_1 (null)) (Term.id `a (null)))))
(Term.depArrow
(Term.explicitBinder "(" (null `α) (null ":" (Term.type "Type" (null))) (null) ")")
"→"
(Term.id `α (null)))
(Term.depArrow
(Term.explicitBinder "(" (null `α `β) (null ":" (Term.type "Type" (null))) (null) ")")
"→"
(Term.id `α (null)))
(Term.arrow (Term.type "Type" (null)) "→" (Term.arrow (Term.type "Type" (null)) "→" (Term.type "Type" (null))))
(Term.depArrow
(Term.explicitBinder "(" (null `α) (null ":" (Term.type "Type" (null))) (null) ")")
"→"
(Term.arrow (Term.id `α (null)) "→" (Term.id `α (null))))
(Term.depArrow
(Term.explicitBinder "(" (null `α) (null ":" (Term.type "Type" (null))) (null) ")")
"→"
(Term.depArrow
(Term.explicitBinder "(" (null `a) (null ":" (Term.id `α (null))) (null) ")")
"→"
(Term.app (Term.id `Eq (null)) (null (Term.id `a (null)) (Term.id `a (null))))))
(Term.depArrow (Term.implicitBinder "{" (null `α) (null ":" (Term.type "Type" (null))) "}") "→" (Term.id `α (null)))
(Term.depArrow
(Term.implicitBinder "{" (null `α) (null ":" (Term.type "Type" (null))) "}")
"→"
(Term.depArrow
(Term.instBinder "[" (null `_inst_1 ":") (Term.app (Term.id `HasToString (null)) (null (Term.id `α (null)))) "]")
"→"
(Term.id `α (null))))
(Term.num (numLit "0"))
(Term.num (numLit "1"))
(Term.num (numLit "42"))
(Term.str (strLit "\"hi\""))
(Term.proj
(Term.paren
"("
(null (Term.app (Term.id `Prod.mk (null)) (null (Term.num (numLit "1")) (Term.num (numLit "2")))) (null))
")")
"."
`fst)
(Term.app
(Term.id `or (null))
(null
(Term.paren
"("
(null (Term.app (Term.id `HasLess.Less (null)) (null (Term.num (numLit "1")) (Term.num (numLit "2")))) (null))
")")
(Term.id `Bool.true (null))))
Reference in a new issue View git blame Copy permalink