Idris2/tests/idris2/interface021/LocalHint.idr

Gnu : Type
Gnu = Int

Foo : Type
Foo = Bool

A : Foo
A = True

mkFoo : Gnu -> Foo
mkFoo gnu = A

gnat : {auto startHere : (a : Foo ** a = A)} -> Unit
gnat = ()

%logging 0
pathology : (gnu : Gnu) -> Unit
pathology gnu =
  let %hint foo : Foo
      foo = mkFoo gnu
      %hint bar : Foo -> (ford : arg = A)
                      -> (a : Foo ** a = A)
      bar _ Refl = (A ** Refl)
  in gnat
%logging 0
Treat local hints differently in auto search Local hints need to reduce (just like global hints do) so we expand their definition to the lifted name before applying them. We're identifying the global hints by knowing that the binder name is a nested function name. This is a bit of hack, and it'd probably be better to record that information in the binder instead, but that's a more substantial change than I want to do right now. 2020-12-27 16:41:48 +03:00			`Gnu : Type`
			`Gnu = Int`

			`Foo : Type`
			`Foo = Bool`

			`A : Foo`
			`A = True`

			`mkFoo : Gnu -> Foo`
			`mkFoo gnu = A`
Remove trailing whitespaces and add trailing newlines 2021-01-16 10:03:45 +03:00
Treat local hints differently in auto search Local hints need to reduce (just like global hints do) so we expand their definition to the lifted name before applying them. We're identifying the global hints by knowing that the binder name is a nested function name. This is a bit of hack, and it'd probably be better to record that information in the binder instead, but that's a more substantial change than I want to do right now. 2020-12-27 16:41:48 +03:00			`gnat : {auto startHere : (a : Foo ** a = A)} -> Unit`
			`gnat = ()`

			`%logging 0`
			`pathology : (gnu : Gnu) -> Unit`
			`pathology gnu =`
			`let %hint foo : Foo`
			`foo = mkFoo gnu`
			`%hint bar : Foo -> (ford : arg = A)`
			`-> (a : Foo ** a = A)`
			`bar _ Refl = (A ** Refl)`
			`in gnat`
			`%logging 0`