max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

test: for issue #1301

Browse source 
closes #1301
This commit is contained in:
Leonardo de Moura 2022-07-13 06:04:33 -07:00
parent 123fd801cb
commit cce2d3500e
2 changed files with 18 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
tests/lean/1301.lean Normal file
View file

@ -0,0 +1,10 @@
syntax "tac" : tactic
theorem a : True := by tac
#check a -- should be declared
theorem a' : True ∧ True := ⟨by tac, by tac⟩
#check a' -- should be declared
syntax "term" : term
def b (n : Nat) : Nat := term
#print b -- should be declared

8
tests/lean/1301.lean.expected.out Normal file
View file

@ -0,0 +1,8 @@
1301.lean:2:23-2:26: error: tactic 'tacticTac' has not been implemented
a : True
1301.lean:5:32-5:35: error: tactic 'tacticTac' has not been implemented
a' : True ∧ True
1301.lean:9:25-9:29: error: elaboration function for 'termTerm' has not been implemented
term
def b : Nat → Nat :=
sorryAx (Nat → Nat) true