Simplifying implicit arguments

Stream: new members

[lxsameer]

Hy folks, is there any way to simplify the implicit arguments of the app constructor? what's the best practice here?

inductive Expr : {n : Nat} -> (t : SType n) -> Type n where
  | atom (s : String) : Expr SType.symbol
  | fn { n m : Nat } {t : SType n } {t' : SType m} : (a : Expr t) -> (b : Expr t') -> Expr (SType.pie t t')
  | app { n m : Nat } {t : SType n } {t'm : SType m} : (f : Expr (SType.pie t t')) -> Expr t -> Expr t'
deriving Repr

{ n m : Nat } {t : SType n } {t' : SType m} is a pattern that I have to keep repeating.

[Aaron Liu]

You could try autoImplicit

[Henrik Böving]

Also note that the n from your n : Nat is not the same n as in your Type n. Universe variables and normal variables are distinct.

[lxsameer]

Thank you, yes I'm aware of that

[Matt Diamond]

what's the purpose of the Nats in your code, then?

[lxsameer]

What do you mean? I'm trying to model simple universes without using lean's universes. (the purpose, is me to learn more about lean and dependent type theory)

[Matt Diamond]

oh whoops, I saw SType and thought it was Type... I see what you're doing now

[Matt Diamond]

sorry!

[Tomas Skrivan]

Maybe I'm misunderstanding the question but are you also aware of the variable command?

[lxsameer]

variable like Agda's variable?

[Matt Diamond]

he means that you can write this:

variable { n m : Nat } {t : SType n } {t' : SType m}

and they will be automatically inserted as assumptions into all functions below

I'm not sure if that applies to constructor arguments, though...

[Eric Wieser]

Yeah, it will do the wrong thing for constructors

[Eric Wieser]

Could you make this a #mwe by including SType?

[lxsameer]

Here is the mwe:

import Std.Data.HashMap

inductive SType : (n : Nat) -> Type n
  | universe : SType n
  | symbol : SType 0
  | pie {n m : Nat } (t : SType n) (t' : SType m) : SType (max n m)
  | sigma {n m : Nat } (t : SType n) (t' : SType m) : SType (max n m)
deriving Repr


inductive Expr : {n : Nat} -> (t : SType n) -> Type n where
  | atom : (s : String) -> Expr SType.symbol
  | app : Expr (SType.pie t t') -> Expr t -> Expr t'
deriving Repr

inductive Value : {n : Nat} -> (t: SType n) -> Type n where
  | fn : (arg : Expr t) -> (body : Expr t') -> Value (SType.pie t t')
  | type : Value t
deriving Repr

inductive TypedValue : Type where
  | mk : Value t → TypedValue
deriving Repr

structure Context where
  env : Std.HashMap String TypedValue := Std.HashMap.empty
  depth : Nat := 0
deriving Repr

def define (ctx : Context) (name : String) (value : Value t) : Context :=
  { ctx with
    env := ctx.env.insert name (TypedValue.mk value)
  }

def lookup (ctx : Context) (name : String) : Option TypedValue :=
  ctx.env.get? name