-
Notifications
You must be signed in to change notification settings - Fork 1
Expand file tree
/
Copy pathProofForgeV2.lean
More file actions
137 lines (137 loc) · 6.22 KB
/
Copy pathProofForgeV2.lean
File metadata and controls
137 lines (137 loc) · 6.22 KB
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
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
import ProofForgeV2.Core.Common
import ProofForgeV2.Core.Unicode
import ProofForgeV2.Core.TargetIdentityV1
import ProofForgeV2.Core.Diagnostic
import ProofForgeV2.Core.DiagnosticV1
import ProofForgeV2.Core.DiagnosticBundleV1
import ProofForgeV2.Source.SpanV1
import ProofForgeV2.Source.WireV1
import ProofForgeV2.Source.NameComponentV1
import ProofForgeV2.Source.QualifiedNameV1
import ProofForgeV2.Source.WireCodecV1
import ProofForgeV2.Source.WireDecodeV1
import ProofForgeV2.Source.AstV1
import ProofForgeV2.Source.AstCodecV1
import ProofForgeV2.Source.AstScalarDecodeV1
import ProofForgeV2.Source.DecodeBudgetV1
import ProofForgeV2.Source.AstTypeDecodeV1
import ProofForgeV2.Source.AstSupportV1
import ProofForgeV2.Source.AstSupportCodecV1
import ProofForgeV2.Source.AstSupportDecodeV1
import ProofForgeV2.Source.AstPatternV1
import ProofForgeV2.Source.AstPatternCodecV1
import ProofForgeV2.Source.AstPatternDecodeV1
import ProofForgeV2.Source.AstDeclV1
import ProofForgeV2.Source.AstDeclCodecV1
import ProofForgeV2.Source.AstDeclDecodeV1
import ProofForgeV2.Source.AstSpineV1
import ProofForgeV2.Source.AstSpineEqV1
import ProofForgeV2.Source.AstSpineCodecV1
import ProofForgeV2.Source.AstSpineDecodeV1
import ProofForgeV2.Source.AstSpineStmtDecodeV1
import ProofForgeV2.Source.AstSpineDeclV1
import ProofForgeV2.Source.AstSpineDeclCodecV1
import ProofForgeV2.Source.AstSpineDeclDecodeV1
import ProofForgeV2.Source.AstProgramItemV1
import ProofForgeV2.Source.AstProgramItemCodecV1
import ProofForgeV2.Source.AstProgramItemDecodeV1
import ProofForgeV2.Source.AstProgramV1
import ProofForgeV2.Source.AstProgramCodecV1
import ProofForgeV2.Source.AstProgramDecodeV1
import ProofForgeV2.Source.AstCanonicalRootV1
import ProofForgeV2.Source.AstProgramValidateV1
import ProofForgeV2.Source.ValidatedSourceV1
import ProofForgeV2.Source.AstCanonicalRootDecodeV1
import ProofForgeV2.Source.NodeTraversalV1
import ProofForgeV2.Source.SpanJoinV1
import ProofForgeV2.Source.NodeAssignmentV1
import ProofForgeV2.Source.OriginJoinV1
import ProofForgeV2.Source.DiagnosticLocateV1
import ProofForgeV2.Frontend.ProtocolV1
import ProofForgeV2.Frontend.WorkerV1
import ProofForgeV2.Typed.DiagnosticDraftV1
import ProofForgeV2.Typed.ModelV1
import ProofForgeV2.Typed.NameResolutionV1
import ProofForgeV2.Typed.TypeCheckV1
import ProofForgeV2.Typed.CallGraphV1
import ProofForgeV2.Typed.EffectCheckV1
import ProofForgeV2.Typed.BoundCheckV1
import ProofForgeV2.Typed.DisclosureCheckV1
import ProofForgeV2.Typed.AuthorityCustodyCheckV1
import ProofForgeV2.Typed.ContextExtensionCheckV1
import ProofForgeV2.Typed.RequirementsInferV1
import ProofForgeV2.Typed.CheckV1
import ProofForgeV2.Semantic.WireV1
import ProofForgeV2.Semantic.ProofBridgeV1
import ProofForgeV2.Semantic.SubjectDataBridgeV1
import ProofForgeV2.Semantic.FieldComparisonSubjectV1
import ProofForgeV2.Semantic.FieldComparisonPreservationV1
import ProofForgeV2.Semantic.InitializerDepositWithdrawViewEqualitySubjectV1
import ProofForgeV2.Semantic.InitializerDepositWithdrawViewEqualityPreservationV1
import ProofForgeV2.Semantic.InitializerDepositViewEqualitySubjectV1
import ProofForgeV2.Semantic.InitializerDepositViewEqualityPreservationV1
import ProofForgeV2.Semantic.InitializerViewEqualitySubjectV1
import ProofForgeV2.Semantic.InitializerViewEqualityPreservationV1
import ProofForgeV2.Semantic.StatefulEqualitySubjectV1
import ProofForgeV2.Semantic.StatefulEqualityPreservationV1
import ProofForgeV2.Semantic.InvariantABI
import ProofForgeV2.Semantic.SimpleClosureCertV1
import ProofForgeV2.Semantic.AuthorWireCertV1
import ProofForgeV2.Semantic.SimpleClosureTraceV1
import ProofForgeV2.Semantic.SimpleClosureStructureCertV1
import ProofForgeV2.Semantic.SimpleClosureEncodeV1
import ProofForgeV2.Semantic.SimpleClosureEncodeFieldsV1
import ProofForgeV2.Semantic.SimpleClosureDecodeV1
import ProofForgeV2.Semantic.SimpleClosureDecodeComposeV1
import ProofForgeV2.Semantic.ReferenceV1
import ProofForgeV2.Semantic.OutcomeWireV1
import ProofForgeV2.Semantic.StateModelV1
import ProofForgeV2.Semantic.PreservationABI
import ProofForgeV2.Semantic.PreservationPackagingV1
import ProofForgeV2.Semantic.PreservationShapeV1
import ProofForgeV2.Semantic.UInt64ParityPreservationV1
import ProofForgeV2.Semantic.UInt64ParitySubjectV1
import ProofForgeV2.Semantic.ProofBundleV1
import ProofForgeV2.Semantic.InlineProofPolicyV1
import ProofForgeV2.Semantic.ProofSubjectV1
import ProofForgeV2.Semantic.ProofReferenceJoinV1
import ProofForgeV2.Compiler.ProofSubjectFilesV1
import ProofForgeV2.Compiler.ProofBundleFilesV1
import ProofForgeV2.Compiler.InlineProofAuditV1
import ProofForgeV2.Compiler.ProofWorkerProtocolV1
import ProofForgeV2.Compiler.ProofWorkerV1
import ProofForgeV2.Compiler.ProofWorkerControlV2
import ProofForgeV2.Compiler.ProofWorkerSupervisorV1
import ProofForgeV2.Compiler.InlineProofProtocolV1
import ProofForgeV2.Compiler.InlineProofElaborationV1
import ProofForgeV2.Compiler.InlineProofCertifierV1
import ProofForgeV2.Compiler.Pipeline
import ProofForgeV2.Language.Syntax
import ProofForgeV2.Language.ProgramElaborationV1
import ProofForgeV2.Language.TheoremInventoryV1
import ProofForgeV2.Language.Loader
import ProofForgeV2.Materialization.Protocol
import ProofForgeV2.Materialization.MaterializedArtifactsV1
import ProofForgeV2.Materialization.ArtifactContentV1
import ProofForgeV2.Materialization.LockedToolchainV1
import ProofForgeV2.Materialization.EngineeringFinalizationV1
import ProofForgeV2.Materialization.EngineeringDiskClosureV1
import ProofForgeV2.Materialization.OutputSetV1
import ProofForgeV2.Examples.StateCell
import ProofForgeV2.Examples.Accumulator
import ProofForgeV2.Examples.PrivateSum4
import ProofForgeV2.Targets.BuildSelectionV1
import ProofForgeV2.Targets.TargetRegistryV1
import ProofForgeV2.Targets.BuildIdentityV1
import ProofForgeV2.Targets.RegistryRootV1
import ProofForgeV2.Targets.RequirementResolverV1
import ProofForgeV2.Targets.SupportClaimV1
import ProofForgeV2.Targets.EngineeringBuildIdentityV1
import ProofForgeV2.Targets.DescriptorDataV1
import ProofForgeV2.Targets.EngineeringBuildV1
import ProofForgeV2.Targets.Registry
import ProofForgeV2.CLI.Emit
import ProofForgeV2.Targets.Near.WasmCertWireV1
import ProofForgeV2.Targets.Near.WasmCertArtifactsV1
import ProofForgeV2.Targets.Near.WasmCertProductV1
import ProofForgeV2.Targets.Near.WasmCertReferenceJoinV1