search

leanprover-community / lean4game

Server to host lean games.
https://adam.math.hhu.de
GNU General Public License v3.0
198 stars 35 forks source link

Structural recursion in `Branch` #70

Open joneugster opened 1 year ago

joneugster commented 1 year ago

This example compiles fine:

Statement MyNat.one_mul (m : ℕ): 1 * m = m := by
  Branch
    rw [MyNat.one_mul]
  sorry

while this one throws the structural recursion error:

Statement MyNat.one_mul (m : ℕ): 1 * m = m := by
  Branch
    rw [MyNat.one_mul]
    done
  sorry

Should get Branch to throw an error in the first case.