Skip to content

Latest commit

 

History

History
 
 

test

Folders and files

NameName
Last commit message
Last commit date

parent directory

..
Mathlib
Mathlib
 
 
all_tactics.expected.out
all_tactics.expected.out
 
 
all_tactics.in
all_tactics.in
 
 
by_cases.expected.out
by_cases.expected.out
 
 
by_cases.in
by_cases.in
 
 
by_cases.lean
by_cases.lean
 
 
calc.expected.out
calc.expected.out
 
 
calc.in
calc.in
 
 
def_eval.expected.out
def_eval.expected.out
 
 
def_eval.in
def_eval.in
 
 
dup_msg.expected.out
dup_msg.expected.out
 
 
dup_msg.in
dup_msg.in
 
 
dup_sorries.expected.out
dup_sorries.expected.out
 
 
dup_sorries.in
dup_sorries.in
 
 
enableInitializersExecution.expected.out
enableInitializersExecution.expected.out
 
 
enableInitializersExecution.in
enableInitializersExecution.in
 
 
file.expected.out
file.expected.out
 
 
file.in
file.in
 
 
file.lean
file.lean
 
 
have_by_sorry.expected.out
have_by_sorry.expected.out
 
 
have_by_sorry.in
have_by_sorry.in
 
 
import_lean.in
import_lean.in
 
 
incomplete.expected.out
incomplete.expected.out
 
 
incomplete.in
incomplete.in
 
 
incomplete.lean
incomplete.lean
 
 
infotree.expected.out
infotree.expected.out
 
 
infotree.in
infotree.in
 
 
invalid_tactic.expected.out
invalid_tactic.expected.out
 
 
invalid_tactic.in
invalid_tactic.in
 
 
name_generator.expected.out
name_generator.expected.out
 
 
name_generator.in
name_generator.in
 
 
no_goal_sorry.expected.out
no_goal_sorry.expected.out
 
 
no_goal_sorry.in
no_goal_sorry.in
 
 
no_goal_sorry_2.expected.out
no_goal_sorry_2.expected.out
 
 
no_goal_sorry_2.in
no_goal_sorry_2.in
 
 
options.expected.out
options.expected.out
 
 
options.in
options.in
 
 
pickle_environment.expected.out
pickle_environment.expected.out
 
 
pickle_environment.in
pickle_environment.in
 
 
pickle_environment_with_imports.expected.out
pickle_environment_with_imports.expected.out
 
 
pickle_environment_with_imports.in
pickle_environment_with_imports.in
 
 
pickle_open.expected.out
pickle_open.expected.out
 
 
pickle_open.in
pickle_open.in
 
 
pickle_open_2.expected.out
pickle_open_2.expected.out
 
 
pickle_open_2.in
pickle_open_2.in
 
 
pickle_open_scoped.expected.out
pickle_open_scoped.expected.out
 
 
pickle_open_scoped.in
pickle_open_scoped.in
 
 
pickle_open_scoped_2.expected.out
pickle_open_scoped_2.expected.out
 
 
pickle_open_scoped_2.in
pickle_open_scoped_2.in
 
 
pickle_proof_state_1.expected.out
pickle_proof_state_1.expected.out
 
 
pickle_proof_state_1.in
pickle_proof_state_1.in
 
 
pickle_proof_state_2.expected.out
pickle_proof_state_2.expected.out
 
 
pickle_proof_state_2.in
pickle_proof_state_2.in
 
 
pickle_proof_state_env.expected.out
pickle_proof_state_env.expected.out
 
 
pickle_proof_state_env.in
pickle_proof_state_env.in
 
 
pickle_scoped_notation.in
pickle_scoped_notation.in
 
 
pickle_scoped_notation_2.in
pickle_scoped_notation_2.in
 
 
proof_step.expected.out
proof_step.expected.out
 
 
proof_step.in
proof_step.in
 
 
readme.expected.out
readme.expected.out
 
 
readme.in
readme.in
 
 
sorry_hypotheses.expected.out
sorry_hypotheses.expected.out
 
 
sorry_hypotheses.in
sorry_hypotheses.in
 
 
synthesize_placeholder.expected.out
synthesize_placeholder.expected.out
 
 
synthesize_placeholder.in
synthesize_placeholder.in
 
 
tactic_mode_sorry.expected.out
tactic_mode_sorry.expected.out
 
 
tactic_mode_sorry.in
tactic_mode_sorry.in
 
 
tactic_sorry.expected.out
tactic_sorry.expected.out
 
 
tactic_sorry.in
tactic_sorry.in
 
 
term_sorry.expected.out
term_sorry.expected.out
 
 
term_sorry.in
term_sorry.in
 
 
trace_simp.expected.out
trace_simp.expected.out
 
 
trace_simp.in
trace_simp.in
 
 
unfinished_tactic_block.expected.out
unfinished_tactic_block.expected.out
 
 
unfinished_tactic_block.in
unfinished_tactic_block.in
 
 
unknown_environment.expected.out
unknown_environment.expected.out
 
 
unknown_environment.in
unknown_environment.in
 
 
unknown_proof_state.expected.out
unknown_proof_state.expected.out
 
 
unknown_proof_state.in
unknown_proof_state.in
 
 
unknown_tactic.expected.out
unknown_tactic.expected.out
 
 
unknown_tactic.in
unknown_tactic.in
 
 
variables.expected.out
variables.expected.out
 
 
variables.in
variables.in
 
 

readme.in

{"cmd" : "def f (x : Unit) : Nat := by sorry"}

{"tactic": "apply Int.natAbs", "proofState": 0}

{"tactic": "exact -37", "proofState": 1}