-
Notifications
You must be signed in to change notification settings - Fork 9
/
Yatima.lean
54 lines (54 loc) · 1.73 KB
/
Yatima.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
import Yatima.Cli.CodeGenCmd
import Yatima.Cli.ContAddrCmd
import Yatima.Cli.GenTypecheckerCmd
import Yatima.Cli.GetCmd
import Yatima.Cli.IpfsCmd
import Yatima.Cli.PinCmd
import Yatima.Cli.ProveCmd
import Yatima.Cli.PutCmd
import Yatima.Cli.TypecheckCmd
import Yatima.Cli.Utils
import Yatima.CodeGen.CodeGen
import Yatima.CodeGen.CodeGenM
import Yatima.CodeGen.Override
import Yatima.CodeGen.Overrides.All
import Yatima.CodeGen.Overrides.Array
import Yatima.CodeGen.Overrides.Bool
import Yatima.CodeGen.Overrides.ByteArray
import Yatima.CodeGen.Overrides.Char
import Yatima.CodeGen.Overrides.Decidable
import Yatima.CodeGen.Overrides.Fin
import Yatima.CodeGen.Overrides.HashMap
import Yatima.CodeGen.Overrides.Int
import Yatima.CodeGen.Overrides.List
import Yatima.CodeGen.Overrides.Miscellaneous
import Yatima.CodeGen.Overrides.Name
import Yatima.CodeGen.Overrides.Nat
import Yatima.CodeGen.Overrides.String
import Yatima.CodeGen.Overrides.Thunk
import Yatima.CodeGen.Overrides.Typechecker
import Yatima.CodeGen.Overrides.UInt
import Yatima.CodeGen.Preloads
import Yatima.CodeGen.PrettyPrint
import Yatima.CodeGen.Simp
import Yatima.Common.GenTypechecker
import Yatima.Common.IO
import Yatima.Common.LightData
import Yatima.Common.ToLDON
import Yatima.ContAddr.ContAddr
import Yatima.ContAddr.ContAddrError
import Yatima.ContAddr.ContAddrM
import Yatima.Datatypes.Const
import Yatima.Datatypes.Env
import Yatima.Datatypes.Expr
import Yatima.Datatypes.Lean
import Yatima.Datatypes.Univ
import Yatima.Lean.LCNF
import Yatima.Lean.Utils
import Yatima.Typechecker.Datatypes
import Yatima.Typechecker.Equal
import Yatima.Typechecker.Eval
import Yatima.Typechecker.Infer
import Yatima.Typechecker.Printing
import Yatima.Typechecker.TypecheckM
import Yatima.Typechecker.Typechecker