Zulip Chat Archive

Stream: new members

Topic: Fix argument with tactic

Horatiu Cheval (Apr 27 2021 at 18:05):

I have defined something along the lines below. Then I noticed that in many cases I provide the context.nth i = some σ argument of var simply with by simp, like in the example at the end. Due to this, I want to define some var' to be var in which the second explicit argument is fixed as by simp. Can this be done?

import tactic

@[derive decidable_eq]
inductive type
| ground : type
| arrow : type  type  type

def context := list type

inductive term : context  type  Type
| var {ctx : context} {σ : type} : Π (i : ), ctx.nth i = some σ  term ctx σ

variables {σ τ : type}
def v₀ : term [σ, τ] σ := term.var 0 (by simp)

Mario Carneiro (Apr 27 2021 at 18:09):

Notations can do that:

notation `#` n := term.var n (by simp)

variables {σ τ : type}
def v₀ : term [σ, τ] σ := #0

Horatiu Cheval (Apr 27 2021 at 18:15):

Right, thanks!

Last updated: Dec 20 2023 at 11:08 UTC