New answers tagged

3

It is true that Agda currently has a much shakier foundation than say Coq or Lean. It does have an internal term syntax that could be seen as a core language (https://github.com/agda/agda/blob/master/src/full/Agda/Syntax/Internal.hs). It even has an independent typechecker for internal syntax (https://github.com/agda/agda/blob/master/src/full/Agda/...


Top 50 recent answers are included