Check for copyright header

fix: `get_elem_tactic_trivial` to not loop in the presence of mvars #3992

Sign in to view logs

Triggered via pull request August 21, 2024 18:06

nomeata

opened #5119

joachim/issue5061

Status Success

Total duration 32s

Artifacts –

copyright-header.yml

on: pull_request

check-lean-files